package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.vernac/ComAssumption/index.html
Module ComAssumptionSource
Parameters/Assumptions
Source
val declare_variable :
coe:Vernacexpr.coercion_flag ->
kind:Decls.assumption_object_kind ->
univs:UState.named_universes_entry ->
impargs:Impargs.manual_implicits ->
impl:Glob_term.binding_kind ->
name:Names.variable ->
Constr.types ->
Names.GlobRef.t * UVars.Instance.tDeclaration of a local assumption (Variable/Hypothesis)
Source
val declare_local :
coe:Vernacexpr.coercion_flag ->
try_assum_as_instance:bool ->
kind:Decls.logical_kind ->
univs:UState.named_universes_entry ->
impargs:Impargs.manual_implicits ->
impl:Glob_term.binding_kind ->
name:Names.variable ->
Constr.constr option ->
Constr.types ->
Names.GlobRef.t * UVars.Instance.tDeclaration of a local construction (Variable/Hypothesis/Let)
Source
val declare_axiom :
coe:Vernacexpr.coercion_flag ->
local:Locality.import_status ->
kind:Decls.assumption_object_kind ->
?user_warns:UserWarn.t ->
univs:UState.named_universes_entry ->
impargs:Impargs.manual_implicits ->
inline:Declaremods.inline ->
name:Names.variable ->
Constr.types ->
Names.GlobRef.t * UVars.Instance.tDeclaration of a global assumption (Axiom/Parameter)
Source
val declare_global :
coe:Vernacexpr.coercion_flag ->
try_assum_as_instance:bool ->
local:Locality.import_status ->
kind:Decls.logical_kind ->
?user_warns:UserWarn.t ->
univs:UState.named_universes_entry ->
impargs:Impargs.manual_implicits ->
inline:Declaremods.inline ->
name:Names.variable ->
Constr.constr option ->
Constr.types ->
Names.GlobRef.t * UVars.Instance.tDeclaration of a global construction (Axiom/Parameter/Definition)
Source
val do_assumptions :
program_mode:bool ->
poly:bool ->
scope:Locality.definition_scope ->
kind:Decls.assumption_object_kind ->
?user_warns:UserWarn.t ->
inline:Declaremods.inline ->
(Constrexpr.ident_decl list * Constrexpr.constr_expr)
Vernacexpr.with_coercion
list ->
unitInterpret the commands Variable/Hypothesis/Axiom/Parameter
Interpret the command Context
Source
val interp_assumption :
program_mode:bool ->
Environ.env ->
Evd.evar_map ->
Constrintern.internalization_env ->
Constrexpr.local_binder_expr list ->
Constrexpr.constr_expr ->
Evd.evar_map * EConstr.types * Impargs.manual_implicitsInterpret a declaration of the form binders |- typ as a type
Source
val interp_context :
Environ.env ->
Evd.evar_map ->
Constrexpr.local_binder_expr list ->
Evd.evar_map
* (Names.Id.t * Constr.t option * Constr.t * Glob_term.binding_kind) listThe first half of the context command, returning the declarations in the same order as Context, using de Bruijn indices (used by Elpi)
On This Page