package rocq-lean-import
Plugin allowing Rocq to import Lean exported files
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.1.tar.gz
sha512=db2d8767129a362822463fc331c19c204b2b1f60784b999a663d93ddc047096b1cec08dc65066f7f58e51039500769e1c073a78756af9cd62c4abc63d779c3ea
Description
Plugin allowing Rocq to import Lean exported files.
Dependencies (2)
- rocq-stdlib
-
ocaml
>= "4.09.0"
Dev Dependencies (1)
-
rocq-core
(>= "9.1~" & < "9.2~") | = "dev"
Used by
None
Conflicts
None
On This Page