package rocq-num-analysis-subset
Subsets for numerical analysis in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-num-analysis-2.0.0.tar.gz
sha512=b2453dc67f2b716ea0a473ca9942eacd3e1eed29493395e35eac5b997e840ec95ed4b028a416b1e92c9a88403cf01812f7744fbc1f0dc8fa8596a2d5c4b8b9b1
Description
This library provides support about subsets, functions, homogeneous binary relations, and finite families. It is based on classical logic. Some complements about logic and natural numbers are also provided.
Tags
category:Math/Logic/Set theory date:2025-06 logpath:NumAnalysis.Requisite logpath:NumAnalysis.Logic logpath:NumAnalysis.Numbers logpath:NumAnalysis.Subsets keyword:subset keyword:function keyword:homogeneous binary relation keyword:operation on finite familiesPublished: 23 Jun 2025
Dependencies (4)
-
coq-mathcomp-classical
>= "1.8" & < "1.12~" -
coq-mathcomp-ssreflect
>= "2.3" & < "2.5~" -
rocq-prover
>= "9.0" & < "9.1~" -
coq
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (2)
Conflicts
None
On This Page