package coq-mathcomp-classical
A library for classical logic for mathematical components
Install
Dune Dependency
Authors
Maintainers
Sources
analysis-1.13.0.tar.gz
sha256=c5fb34eafa49c3d5a465db541fc478c83bd866f8fe11024cb1304c1d476801d5
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: 19 Aug 2025
Dependencies (5)
-
coq-hierarchy-builder
(>= "1.8.0") -
coq-mathcomp-finmap
(>= "2.1.0") - coq-mathcomp-algebra
- coq-mathcomp-fingroup
-
coq
>= "8.20" & < "8.21~"
Dev Dependencies (2)
-
coq-mathcomp-ssreflect
(>= "2.3.0" & < "2.5~") | (= "dev") -
coq-core
(>= "9.0" & < "9.1~") | (= "dev")
Used by (6)
Conflicts
None
On This Page