\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module N = Level
+
type ix = int (* index *)
type id = string (* identifier *)
type kind = Decl (* generic declaration *)
| Ax (* axiom *)
+ | Cong (* conjecture *)
| Def (* generic definition *)
| Th (* theorem *)
-type bind = Abst of (id * bool * term) list (* name, real?, domain *)
- | Abbr of (id * term) list (* name, bodies *)
- | Void of id list (* names *)
-
-and term = Sort of ix (* level *)
- | NSrt of id (* named level *)
- | LRef of ix * ix (* index, offset *)
- | NRef of id (* name *)
- | Cast of term * term (* domain, element *)
- | Appl of term list * term (* arguments, function *)
- | Bind of bind * term (* binder, scope *)
- | Inst of term * term list (* function, arguments *)
- | Impl of bool * id * term * term (* strong?, label, source, target *)
-
-type command = Require of id list (* required files: names *)
- | Graph of id (* hierarchy graph: name *)
- | Sorts of (int option * id) list (* sorts: index, name *)
- | Section of id option (* section: Some id = open, None = close last *)
- | Entity of kind * id * desc * term (* entity: class, name, description, contents *)
- | Generate of term list (* predefined generated entity: arguments *)
+type bind =
+(* name, real?, domain *)
+ | Abst of (id * bool * term) list
+(* name, bodies *)
+ | Abbr of (id * term) list
+(* names *)
+ | Void of id list
+
+and term =
+(* level *)
+ | Sort of ix
+(* named level *)
+ | NSrt of id
+(* index, offset *)
+ | LRef of ix * ix
+(* name *)
+ | NRef of id
+(* domain, element *)
+ | Cast of term * term
+(* arguments, function *)
+ | Appl of term list * term
+(* level, binder, scope *)
+ | Bind of N.level * bind * term
+(* function, arguments *)
+ | Inst of term * term list
+(* level, strong?, label, source, target *)
+ | Impl of N.level * bool * id * term * term
+
+type command =
+(* required files: names *)
+ | Require of id list
+(* hierarchy graph: name *)
+ | Graph of id
+(* sorts: index, name *)
+ | Sorts of (int option * id) list
+(* section: Some id = open, None = close last *)
+ | Section of id option
+(* entity: class, name, description, contents *)
+ | Entity of kind * N.level * id * desc * term
+(* predefined generated entity: arguments *)
+ | Generate of term list