package rocq-num-analysis-subset
Subsets for numerical analysis in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-num-analysis-2.2.0.tar.gz
sha512=d1996546d967000045e3c58484d6bda8bf4e153f62d6ee42789090c772f0fede197a41b22cfd8253c2729cec515d0bb834d52904d9a38e656858ee7778aac779
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:Mathematics/Logic/Set theory date:2026-03 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: 13 Mar 2026
Dependencies (6)
-
coq-mathcomp-classical
>= "1.8" & < "1.15~" -
coq-mathcomp-ssreflect
>= "2.3" & < "2.6~" - rocq-stdlib
-
rocq-core
>= "9.0" & < "9.2~" - coq-stdlib
-
coq-core
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (2)
-
rocq-num-analysis-algebra
>= "2.2.0" -
rocq-num-analysis-lebesgue
>= "2.2.0"
Conflicts
None
On This Page