package coq-lean-import
Plugin allowing Coq to import Lean exported files
Install
Dune Dependency
Authors
Maintainers
Sources
v8.20-lean3+alpha.tar.gz
sha512=f8b7bbc6e4ce52e458ca7f2b48c30a5df1c63b1eb4a59a26fff0b7a96f1211298379972e6e799baad3205443e040de3a246e8b90efb266bb5d177e030ab57e25
Description
Plugin allowing Coq to import Lean exported files.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page