From 5d227bcd0055d02e1d49a3dcd27e80a756923d5b Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 23 Jun 2024 23:31:59 +0200 Subject: split code into smaller libraries and make a better repl --- lib/Domain.ml | 30 ------------------------------ 1 file changed, 30 deletions(-) delete mode 100644 lib/Domain.ml (limited to 'lib/Domain.ml') diff --git a/lib/Domain.ml b/lib/Domain.ml deleted file mode 100644 index 6f5e11c..0000000 --- a/lib/Domain.ml +++ /dev/null @@ -1,30 +0,0 @@ -open Bwd - -type t = Data.value = - | Neutral of ne - | Pi of Ident.local * t * clo - | Lam of Ident.local * clo - | Sg of Ident.local * t * clo - | Pair of t * t - | Type - | Bool - | True - | False - -and ne = Data.ne -and ne_head = Data.ne_head = Var of int (* De Bruijn levels *) -and frm = Data.frm = - | App of t - | Fst - | Snd - | BoolElim of { - motive_var : Ident.local; - motive : clo; - true_case : t; - false_case: t; - } - -and env = Data.env -and clo = Data.clo = Clo of { body : Data.syn; env : env } - -let var i = Neutral (Var i, Bwd.Emp) -- cgit 1.4.1