diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/indrec.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/indrec.mli')
-rw-r--r-- | pretyping/indrec.mli | 56 |
1 files changed, 30 insertions, 26 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 102c7c7f..91d559e1 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indrec.mli 11562 2008-11-09 11:30:10Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names @@ -27,36 +27,41 @@ exception RecursionSchemeError of recursion_scheme_error (** Eliminations *) -(* These functions build elimination predicate for Case tactic *) +type dep_flag = bool -val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr -val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr -val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr +(* Build a case analysis elimination scheme in some sort family *) -(* This builds an elimination scheme associated (using the own arity - of the inductive) *) +val build_case_analysis_scheme : env -> evar_map -> inductive -> + dep_flag -> sorts_family -> constr -val build_indrec : env -> evar_map -> inductive -> constr -val instantiate_indrec_scheme : sorts -> int -> constr -> constr -val instantiate_type_indrec_scheme : sorts -> int -> constr -> types -> - constr * types +(* Build a dependent case elimination predicate unless type is in Prop *) -(** Complex recursion schemes [Scheme] *) +val build_case_analysis_scheme_default : env -> evar_map -> inductive -> + sorts_family -> constr -val build_mutual_indrec : - env -> evar_map -> - (inductive * mutual_inductive_body * one_inductive_body - * bool * sorts_family) list - -> constr list +(* Builds a recursive induction scheme (Peano-induction style) in the same + sort family as the inductive family; it is dependent if not in Prop *) -(** Old Case/Match typing *) +val build_induction_scheme : env -> evar_map -> inductive -> + dep_flag -> sorts_family -> constr -val type_rec_branches : bool -> env -> evar_map -> inductive_type - -> constr -> constr -> constr array * constr -val make_rec_branch_arg : - env -> evar_map -> - int * ('b * constr) option array * int -> - constr -> constructor_summary -> wf_paths list -> constr +(* Builds mutual (recursive) induction schemes *) + +val build_mutual_induction_scheme : + env -> evar_map -> (inductive * dep_flag * sorts_family) list -> constr list + +(** Scheme combinators *) + +(* [modify_sort_scheme s n c] modifies the quantification sort of + scheme c whose predicate is abstracted at position [n] of [c] *) + +val modify_sort_scheme : sorts -> int -> constr -> constr + +(* [weaken_sort_scheme s n c t] derives by subtyping from [c:t] + whose conclusion is quantified on [Type] at position [n] of [t] a + scheme quantified on sort [s] *) + +val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types (** Recursor names utilities *) @@ -64,5 +69,4 @@ val lookup_eliminator : inductive -> sorts_family -> constr val elimination_suffix : sorts_family -> string val make_elimination_ident : identifier -> sorts_family -> identifier - - +val case_suffix : string |