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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4
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)"
>