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_______________________________________________________________ *)
14 exception IllFormedReference of string Lazy.t
18 | Def of int (* height *)
19 | Fix of int * int * int (* fixno, recparamno, height *)
21 | Ind of bool * int * int (* inductive, indtyno, leftno *)
22 | Con of int * int * int (* indtyno, constrno, leftno *)
24 type reference = private Ref of NUri.uri * spec
26 val eq: reference -> reference -> bool
27 val string_of_reference: reference -> string
28 val reference_of_string: string -> reference
30 (* given the reference of an inductive type, returns the i-th contructor *)
31 val mk_constructor: int -> reference -> reference
32 (* given the reference of an inductive type constructor, returns the indty *)
33 val mk_indty: bool -> reference -> reference
34 val mk_fix: int -> int -> reference -> reference
35 val mk_cofix: int -> reference -> reference