package rocq-runtime
On This Page
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824
doc/rocq-runtime.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:Globnames.extended_global_reference UserWarn.with_qf ->
univs:UState.named_universes_entry ->
impargs:Impargs.manual_implicits ->
inline:Declaremods.inline ->
name:Names.lident ->
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:Globnames.extended_global_reference UserWarn.with_qf ->
univs:UState.named_universes_entry ->
impargs:Impargs.manual_implicits ->
inline:Declaremods.inline ->
name:Names.lident ->
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:Globnames.extended_global_reference UserWarn.with_qf ->
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