package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3
doc/coq-core.clib/Int/index.html
Module Int
Source
A native integer module with usual utility functions.
This is a (partial) implementation of a Map
interface on integers, except that it internally uses persistent arrays. This ensures O(1) accesses in non-backtracking cases. It is thus better suited for zero-starting, contiguous keys, or otherwise a lot of space will be empty. To keep track of the present keys, a binary tree is also used, so that adding a key is still logarithmic. It is therefore essential that most of the operations are accesses and not add/removes.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>