package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/extraction_plugin/Extraction_plugin/index.html
Module Extraction_plugin
Source
Big
: a wrapper around ocaml ZArith
with nicer names, and a few extraction-specific constructions
By default, in module Format, you can do horizontal placing of blocks even if they include newlines, as long as the number of chars in the blocks are less that a line length. To avoid this awkward situation, we attach a big virtual size to fnl
newlines.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>