package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42
doc/coq-core.clib/CString/Pred/index.html
Module CString.Pred
Source
The type of sets.
add x s
returns a set containing all elements of s
, plus x
. If x
was already in s
, then s
is returned unchanged.
remove x s
returns a set containing all elements of s
, except x
. If x
was not in s
, then s
is returned unchanged.
equal s1 s2
tests whether the sets s1
and s2
are equal, that is, contain equal elements.
Gives a finite representation of the predicate: if the boolean is false, then the predicate is given in extension. if it is true, then the complement is given
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>