(****
 *
 * NOTE: This example has to be run from two separate files to have the
 * intended affect, since all val decls are processed before any execution
 * takes place.  Hence, it's been broken up into the two files
 * quantifier_forall_{false,true}_example.fmsl.  Alternatively, the value decls
 * can be replaced with let exprs to obtain the intended effect.
 *
 *)

(*
 * Create values p1 and p2, which puts them in the Person type value universe.
 *)
val p1:Person = {"Alan", "Turing", 97};
val p2:Person = {"Arnold", "Schwarzenegger", 61};
> forall (p:Person) p.last != nil;             -- evaluates to true

(* 
 * Create a value p3 with nil last name, and re-evaluate the quantifier.
 *)
val p3:Person = {"Charles", nil, 218};
> forall (p:Person) p.last != nil;             -- now evaluates to false