package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module IndschemesSource

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

Sourceval name_and_process_schemes : Environ.env -> (Names.lident option * Vernacexpr.scheme) list -> resolved_scheme list

Resolve the names of a list of inductive schemes with respect to an environment

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.

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

Main calls to interpret the Scheme command

Sourceval 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

Sourceval 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct