package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.0.tar.gz

sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.vernac/Indschemes/index.html

Module `Indschemes`Source

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

Build and register the boolean equalities associated to an inductive type

Sourceval declare_beq_scheme : Names.MutInd.t -> unit

Sourceval declare_eq_decidability : Names.MutInd.t -> unit

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

Sourceval declare_congr_scheme : Names.inductive -> unit

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

Sourceval declare_rewriting_schemes : 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.

Source

val do_mutual_induction_scheme : 
  ?force_mutual:bool ->
  (Names.lident * bool * Names.inductive * Sorts.family) list ->
  unit

Main calls to interpret the Scheme command

Sourceval do_scheme : (Names.lident option * Vernacexpr.scheme) list -> unit

Combine a list of schemes into a conjunction of them

Source

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

Sourceval do_combined_scheme : Names.lident -> Names.lident list -> unit

Hook called at each inductive type definition

Sourceval declare_default_schemes : Names.MutInd.t -> unit