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

  value : exp -> type.  %name value P.

  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).