diff options
Diffstat (limited to 'lib/Data.ml')
-rw-r--r-- | lib/Data.ml | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/lib/Data.ml b/lib/Data.ml deleted file mode 100644 index d2f94d3..0000000 --- a/lib/Data.ml +++ /dev/null @@ -1,53 +0,0 @@ -open Bwd - -(** Syntactic terms *) - -type syn = - | Var of int - | Pi of Ident.local * syn * (* BINDS *) syn - | Lam of Ident.local * (* BINDS *) syn - | App of syn * syn - | Sg of Ident.local * syn * (* BINDS *) syn - | Pair of syn * syn - | Fst of syn - | Snd of syn - | Type - | Bool - | True - | False - | BoolElim of { - motive_var : Ident.local; - motive : (* BINDS *) syn; - true_case : syn; - false_case : syn; - scrut : syn; - } - -(** Semantic domain *) - -type value = - | Neutral of ne - | Pi of Ident.local * value * clo - | Lam of Ident.local * clo - | Sg of Ident.local * value * clo - | Pair of value * value - | Type - | Bool - | True - | False - -and ne = ne_head * frm bwd -and ne_head = Var of int (* De Bruijn levels *) -and frm = - | App of value - | Fst - | Snd - | BoolElim of { - motive_var : Ident.local; - motive: clo; - true_case: value; - false_case: value; - } - -and env = value bwd -and clo = Clo of { body : syn; env : env } |