package rocq-lean-import
Plugin allowing Rocq to import Lean exported files
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.2.tar.gz
sha512=bd50f013f4fa6885755d2d4ba619408da3c0e58c94b1176b7d873c3be3f4b488d15c6e5b52cde31cc9533801265940051d2b95aac5380a14e87d4489e8324c8d
Description
Plugin allowing Rocq to import Lean exported files.
Dependencies (3)
- rocq-stdlib
-
rocq-core
>= "9.2~" & < "9.3~" -
ocaml
>= "4.09.0"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page