package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
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:Entries.universes_entry ->
role:Evd.side_effect_role ->
name:Names.Id.t ->
Constr.t ->
Names.Constant.t * Evd.side_effects)
ref