diff options
Diffstat (limited to 'kernel/constant.ml')
| -rw-r--r-- | kernel/constant.ml | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/kernel/constant.ml b/kernel/constant.ml index dda7274af..7f45aae57 100644 --- a/kernel/constant.ml +++ b/kernel/constant.ml @@ -7,6 +7,8 @@ open Generic open Term open Sign +(* Constant entries *) + type lazy_constant_value = | Cooked of constr | Recipe of (unit -> constr) @@ -34,3 +36,41 @@ type constant_entry = { const_entry_body : lazy_constant_value; const_entry_type : constr option } +(* Inductive entries *) + +type recarg = + | Param of int + | Norec + | Mrec of int + | Imbr of inductive_path * recarg list + +type mutual_inductive_packet = { + mind_consnames : identifier array; + mind_typename : identifier; + mind_lc : constr; + mind_arity : typed_type; + mind_sort : sorts; + mind_nrealargs : int; + mind_kelim : 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_constraints : constraints; + mind_singl : constr option; + mind_nparams : int } + +let mind_type_finite mib i = mib.mind_packets.(i).mind_finite + +(*s Declaration. *) + +type mutual_inductive_entry = { + mind_entry_nparams : int; + mind_entry_finite : bool; + mind_entry_inds : (identifier * constr * identifier list * constr) list } + +let mind_nth_type_packet mib n = mib.mind_packets.(n) |