package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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

Module `Indschemes`Source

Source

type resolved_scheme =
  Names.Id.t CAst.t * Indrec.dep_flag * Names.inductive * Sorts.family

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

Source

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

Sourceval declare_congr_scheme : ?loc:Loc.t -> Names.inductive -> 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.

Source

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

Main calls to interpret the Scheme command

Source

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

Main call to Scheme Equality command

Source

val do_scheme_equality : 
  ?locmap:Ind_tables.Locmap.t ->
  Vernacexpr.equality_scheme_type ->
  Libnames.qualid Constrexpr.or_by_notation ->
  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.Constant.t list -> unit

Hook called at each inductive type definition

Source

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

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module IndschemesSource

Module `Indschemes`Source