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