diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-15 15:24:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-15 15:24:13 +0000 |
| commit | d44846131cf2fab2d3c45d435b84d802b1af8d43 (patch) | |
| tree | 20de854b9ba4de7cbd01470559e956451a1d5d8e /kernel/inductive.mli | |
| parent | 490c8fa3145e861966dd83f6dc9478b0b96de470 (diff) | |
Nouveaux types 'constructor' et 'inductive' dans Term;
les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 63e85a539..c28d35c8d 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -14,7 +14,7 @@ type recarg = | Param of int | Norec | Mrec of int - | Imbr of section_path * int * (recarg list) + | Imbr of inductive_path * (recarg list) type mutual_inductive_packet = { mind_consnames : identifier array; @@ -63,6 +63,20 @@ val mis_consnames : mind_specif -> identifier array val mind_nth_type_packet : mutual_inductive_body -> int -> mutual_inductive_packet +(* A light version of mind_specif_of_mind with pre-splitted args + Invariant: We have + -- Hnf (fullmind) = DOPN(AppL,[|MutInd mind;..params..;..realargs..|]) + -- with mind = ((sp,i),localvars) for some sp, i, localvars + *) +type inductive_summary = + {fullmind : constr; + mind : inductive; + nparams : int; + nrealargs : int; + nconstr : int; + params : constr list; + realargs : constr list; + arity : constr} (*s Declaration of inductive types. *) @@ -107,4 +121,11 @@ val mind_extract_params : int -> constr -> (name * constr) list * constr val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit -val inductive_of_constructor : constructor_path -> inductive_path +val inductive_of_constructor : constructor -> inductive + +val ith_constructor_of_inductive : inductive -> int -> constructor + +val inductive_path_of_constructor_path : constructor_path -> inductive_path + +val ith_constructor_path_of_inductive_path : + inductive_path -> int -> constructor_path |