package coq-mathcomp-classical

You can search for identifiers within the package.

in-package search v0.2.0

A library for classical logic for mathematical components

Install

Dune Dependency

github.com Edit opam file Versions (24)

Authors

Maintainers

R

Reynald Affeldt <reynald.affeldt@aist.go.jp>

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.classical

Published: 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 (2)

coq-mathcomp-cad
coq-mathcomp-reals >= "1.13.0"

Conflicts

None

On This Page

Description
Dependencies (5)
Dev Dependencies (2)
Used by (2)
Conflicts