From 97f84ccace4e634b4e02178a702818e69292dc9f Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 8 Jul 2024 22:01:42 +0200 Subject: implement top-level definitions --- src/nbe/Syntax.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/nbe/Syntax.ml') diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml index dd690fb..5de5281 100644 --- a/src/nbe/Syntax.ml +++ b/src/nbe/Syntax.ml @@ -1,5 +1,6 @@ type t = Data.syn = | Var of int + | Def of Ident.t * Data.value Lazy.t | Pi of Ident.local * t * (* BINDS *) t | Lam of Ident.local * (* BINDS *) t | App of t * t -- cgit 1.4.1