package coq-mathcomp-classical
A library for classical logic for mathematical components
Install
Dune Dependency
Authors
Maintainers
Sources
analysis-1.10.0.tar.gz
sha512=7be39db1aca5a3c49b2d38167bc1c55c35b64fbe0de69ab22181228aee0366fe039cda21446802d5f8def0190d9bef3fbd9dc0c616505c0c6345372cc94b9ce7
Description
This repository contains a library for classical logic for the Coq proof-assistant and using the Mathematical Components library.
Tags
category:Mathematics/Logic/Classical logic keyword:classical logic keyword:logic keyword:sets keyword:set theory keyword:function keyword:cardinal keyword:filter logpath:mathcomp.classicalPublished: 22 Apr 2025
Dependencies (5)
-
coq-hierarchy-builder
(>= "1.7.0") -
coq-mathcomp-finmap
(>= "2.0.0") - coq-mathcomp-algebra
- coq-mathcomp-fingroup
-
coq-mathcomp-ssreflect
(>= "2.1.0")
Dev Dependencies (1)
-
coq
(>= "8.19" & < "9.1~") | (= "dev")
Used by (2)
- coq-mathcomp-cad
-
coq-mathcomp-reals
>= "1.10.0"
Conflicts
None
On This Page