Commit cb9e6377 authored by POTTIER Francois's avatar POTTIER Francois

Added scratch.ml, which needs cleanup.

parent 89b7b4a0
(* -------------------------------------------------------------------------- *)
(* Sample well-typed terms. *)
let identity =
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"))
let terms : raw_term list = [
identity;
TeTyAbs ("A", TeAbs ("x", TyVar "A",
TeApp (TeTyApp (identity, TyVar "A"), TeVar "x")
));
TeTyAbs ("A", TeAbs ("x", TyVar "A",
TeTyAbs ("B", TeAbs ("y", TyVar "B",
TeLet ("id", identity,
TePair (
TeApp (TeTyApp (TeVar "id", TyVar "A"), TeVar "x"),
TeApp (TeTyApp (TeVar "id", TyVar "B"), TeVar "y")
)
)
))));
]
(* -------------------------------------------------------------------------- *)
(* Sample ill-typed terms. *)
let ill_typed : raw_term list = [
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeApp (TeVar "x", TeVar "x")));
TeProj (1, identity);
TeTyAbs ("A",
TeLet ("id", TeAbs ("x", TyVar "A", TeVar "x"),
TeTyApp (TeVar "id", TyVar "A")
)
);
]
(* TEMPORARY report unbound term variables, with locations. *)
(* TEMPORARY report unbound type variables, with locations. *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment