%%% Definition of Values
%%% Author: Frank Pfenning, based on [Michaylov & Pfenning 92]

value : exp -> type.  %name value P.
%mode value +V.

val_z     : value z.
val_s     : value (s E) <- value E.


val_pair  : value (pair E1 E2) <- value E1 <- value E2.
val_lam   : value (lam E).