package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
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 :
?loc:Loc.t ->
individual scheme_kind ->
Names.Id.t option ->
Names.inductive ->
unitSource
val define_mutual_scheme :
?locmap:Locmap.t ->
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 ->
?loc:Loc.t ->
Constr.t ->
Names.Constant.t * Evd.side_effects)
ref