package rocq-runtime
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759
doc/ring_plugin/Ring_plugin/Ring/index.html
Module Ring_plugin.RingSource
Source
val add_theory :
Names.Id.t ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr Ring_ast.ring_mod list ->
unitSource
val ring_lookup :
Geninterp.Val.t ->
EConstr.constr list ->
EConstr.constr list ->
EConstr.constr ->
unit Proofview.tacticSource
val add_field_theory :
Names.Id.t ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr Ring_ast.field_mod list ->
unitSource
val field_lookup :
Geninterp.Val.t ->
EConstr.constr list ->
EConstr.constr list ->
EConstr.constr ->
unit Proofview.tactic sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>