type uri = NUri.uri
type id = Aut.id
-type bind = Abst | Abbr (* abstraction, abbreviation *)
+type bind = Void (* exclusion *)
+ | Abst of term (* abstraction *)
+ | Abbr of term (* abbreviation *)
-type term = Sort of int (* hierarchy index *)
- | LRef of int (* reverse de Bruijn index *)
- | GRef of uri (* reference *)
- | Cast of term * term (* type, term *)
- | Appl of term * term (* argument, function *)
- | Bind of id * bind * term * term (* name, binder, content, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of int (* reverse de Bruijn index *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* type, term *)
+ | Appl of term * term (* argument, function *)
+ | Bind of id * bind * term (* name, binder, scope *)
-type obj = int * uri * bind * term (* age, uri, binder, contents *)
+type obj = int * uri * bind (* age, uri, binder, contents *)
type item = obj option
(* Currified constructors ***************************************************)
+let abst w = Abst w
+
+let abbr v = Abbr v
+
let cast u t = Cast (u, t)
let appl u t = Appl (u, t)
-let bind id b u t = Bind (id, b, u, t)
+let bind id b t = Bind (id, b, t)