2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 type ix = int (* index *)
14 type id = string (* identifier *)
16 type desc = string (* description *)
18 type kind = Decl (* generic declaration *)
20 | Def (* generic definition *)
23 type bind = Abst of (id * bool * term) list (* name, real?, domain *)
24 | Abbr of (id * term) list (* name, bodies *)
25 | Void of id list (* names *)
27 and term = Sort of ix (* level *)
28 | NSrt of id (* named level *)
29 | LRef of ix * ix (* index, offset *)
30 | NRef of id (* name *)
31 | Cast of term * term (* domain, element *)
32 | Appl of term list * term (* arguments, function *)
33 | Bind of bind * term (* binder, scope *)
34 | Inst of term * term list (* function, arguments *)
35 | Impl of bool * id * term * term (* strong?, label, source, target *)
37 type command = Require of id list (* required files: names *)
38 | Graph of id (* hierarchy graph: name *)
39 | Sorts of (int option * id) list (* sorts: index, name *)
40 | Section of id option (* section: Some id = open, None = close last *)
41 | Entity of kind * id * desc * term (* entity: class, name, description, contents *)
42 | Generate of term list (* predefined generated entity: arguments *)