blob: 7f2887f20082a9bbedfd211440aacac518824855 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(* $Id$ *)
open Names
open Term
open Sign
type recarg =
| Param of int
| Norec
| Mrec of int
| Imbr of section_path * int * (recarg list)
type mutual_inductive_packet = {
mind_consnames : identifier array;
mind_typename : identifier;
mind_lc : constr;
mind_stamp : name;
mind_arity : typed_type;
mind_lamexp : constr option;
mind_kd : sorts list;
mind_kn : sorts list;
mind_listrec : (recarg list) array;
mind_finite : bool }
type mutual_inductive_body = {
mind_kind : path_kind;
mind_ntypes : int;
mind_hyps : typed_type signature;
mind_packets : mutual_inductive_packet array;
mind_singl : constr option;
mind_nparams : int }
type mutual_inductive_entry = section_path * mutual_inductive_body
val mind_type_finite : mutual_inductive_body -> int -> bool
type mind_specif = {
mis_sp : section_path;
mis_mib : mutual_inductive_body;
mis_tyi : int;
mis_args : constr array;
mis_mip : mutual_inductive_packet }
val mis_ntypes : mind_specif -> int
val mis_nconstr : mind_specif -> int
val mis_nparams : mind_specif -> int
val mis_kd : mind_specif -> sorts list
val mis_kn : mind_specif -> sorts list
val mis_recargs : mind_specif -> (recarg list) array array
val mind_nth_type_packet :
mutual_inductive_body -> int -> mutual_inductive_packet
|
