1 files changed, 10 insertions, 6 deletions
diff --git a/src/nbe/Data.ml b/src/nbe/Data.ml
index d2f94d3..8589ea5 100644
--- a/src/nbe/Data.ml
+++ b/src/nbe/Data.ml
@@ -1,9 +1,8 @@
 open Bwd
 
-(** Syntactic terms *)
-
 type syn =
   | Var of int
+  | Def of Ident.t * value Lazy.t
   | Pi of Ident.local * syn * (* BINDS *) syn
   | Lam of Ident.local * (* BINDS *) syn
   | App of syn * syn
@@ -23,10 +22,9 @@ type syn =
       scrut : syn;
     }
 
-(** Semantic domain *)
-
-type value =
+and value =
   | Neutral of ne
+  | Unfold of unfold
   | Pi of Ident.local * value * clo
   | Lam of Ident.local * clo
   | Sg of Ident.local * value * clo
@@ -37,7 +35,13 @@ type value =
   | False
 
 and ne = ne_head * frm bwd
-and ne_head = Var of int (* De Bruijn levels *)
+and ne_head =
+  | Var of int (* De Bruijn levels *)
+
+and unfold = unfold_head * frm bwd * value Lazy.t
+and unfold_head =
+  | Def of Ident.t * value Lazy.t
+
 and frm = 
   | App of value
   | Fst