package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.vernac/Indschemes/index.html

Module IndschemesSource

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

Build and register the boolean equalities associated to an inductive type

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

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

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

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

Main calls to interpret the Scheme command

Sourceval do_scheme : register:bool -> 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 do_combined_scheme : Names.lident -> Names.Constant.t list -> unit
Sourcetype declare_mind_function = ?all_depth:int -> Entries.mutual_inductive_entry -> UState.named_universes_entry -> Names.MutInd.t

Hook called at each inductive type definition

Sourceval declare_default_schemes : ?locmap:Ind_tables.Locmap.t -> ?all_depth:int -> declare_mind:declare_mind_function -> Names.MutInd.t -> unit
Sourcemodule Internal : sig ... end