%%% Mini-ML Natural Semantics
%%% Version restricted to pure lambda-calculus
%%% Author: Frank Pfenning, based on [Michaylov & Pfenning 92]

eval : exp -> exp -> type.  %name eval D.
%mode eval +E -V.

% Functions
ev_lam : eval (lam E) (lam E).
ev_app : eval (app E1 E2) V
	  <- eval E1 (lam E1')
	  <- eval E2 V2
	  <- eval (E1' V2) V.