package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/coq-core.tactics/Ind_tables/index.html
Module Ind_tablesSource
This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand
A scheme is either a "mutual scheme_kind" or an "individual scheme_kind"
Source
type scheme_dependency = | SchemeMutualDep of Names.MutInd.t * mutual scheme_kind| SchemeIndividualDep of Names.inductive * individual scheme_kind
Source
type mutual_scheme_object_function =
Environ.env ->
handle ->
Names.MutInd.t ->
Constr.constr array Evd.in_evar_universe_contextSource
type individual_scheme_object_function =
Environ.env ->
handle ->
Names.inductive ->
Constr.constr Evd.in_evar_universe_contextMain functions to register a scheme builder. Note these functions are not safe to be used by plugins as their effects won't be undone on backtracking
Source
val declare_mutual_scheme_object :
string ->
?deps:(Environ.env -> Names.MutInd.t -> scheme_dependency list) ->
?aux:string ->
mutual_scheme_object_function ->
mutual scheme_kindSource
val declare_individual_scheme_object :
string ->
?deps:(Environ.env -> Names.inductive -> scheme_dependency list) ->
?aux:string ->
individual_scheme_object_function ->
individual scheme_kindForce generation of a (mutually) scheme with possibly user-level names
Source
val define_individual_scheme :
individual scheme_kind ->
Names.Id.t option ->
Names.inductive ->
unitSource
val define_mutual_scheme :
mutual scheme_kind ->
(int * Names.Id.t) list ->
Names.MutInd.t ->
unitMain function to retrieve a scheme in the cache or to generate it
Like find_scheme but does not generate a constant on the fly
Source
val local_lookup_scheme :
handle ->
'a scheme_kind ->
Names.inductive ->
Names.Constant.t optionTo be used by scheme-generating functions when looking for a subscheme.
Source
val declare_definition_scheme :
(internal:bool ->
univs:UState.named_universes_entry ->
role:Evd.side_effect_role ->
name:Names.Id.t ->
Constr.t ->
Names.Constant.t * Evd.side_effects)
ref