Module Indschemes

See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ...

Build and register the boolean equalities associated to an inductive type

val declare_beq_scheme : ?locmap:Ind_tables.Locmap.t -> Names.MutInd.t -> unit
val declare_eq_decidability : ?locmap:Ind_tables.Locmap.t -> Names.MutInd.t -> unit

Build and register a congruence scheme for an equality-like inductive type

val declare_congr_scheme : ?loc:Loc.t -> Names.inductive -> unit

Build and register rewriting schemes for an equality-like inductive type

val declare_rewriting_schemes : ?loc:Loc.t -> Names.inductive -> unit

Mutual Minimality/Induction scheme. force_mutual forces the construction of eliminators having the same predicates and methods even if some of the inductives are not recursive. By default it is false and some of the eliminators are defined as simple case analysis. By default isrec is true.

val do_mutual_induction_scheme : ?force_mutual:bool -> Environ.env -> ?isrec:bool -> resolved_scheme list -> unit

Main calls to interpret the Scheme command

val do_scheme : Environ.env -> (Names.Id.t CAst.t option * Vernacexpr.scheme) list -> unit

Main call to Scheme Equality command

Combine a list of schemes into a conjunction of them

val build_combined_scheme : Environ.env -> Names.Constant.t list -> Evd.evar_map * Constr.constr * Constr.types
val do_combined_scheme : Names.lident -> Names.Constant.t list -> unit

Hook called at each inductive type definition

val declare_default_schemes : ?locmap:Ind_tables.Locmap.t -> Names.MutInd.t -> unit