package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
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.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:Globnames.extended_global_reference UserWarn.with_qf ->
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: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