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

feval : env -> exp' -> val -> type.  %name feval D.
%mode feval +N +F -W.

% Variables
fev_1 : feval (N , W) 1 W.
fev_^ : feval (N , W') (F ^) W
	   <- feval N F W.

% Functions
fev_lam : feval N (lam' F) (clo N (lam' F)).
fev_app : feval N (app' F1 F2) W
	   <- feval N F1 (clo N' (lam' F1'))
	   <- feval N F2 W2
	   <- feval (N' , W2) F1' W.