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 (22)

Authors

Maintainers

R

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

Sources

analysis-1.11.0.tar.gz

sha512=120848a354f1ff91b67d00681338428ba3e405ad18196f20460dd3716295ababa84218d88257e5e85e0d3f8b4c34f135a034bddf155ae53a8776f114b742ef7f

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: 02 May 2025

Dependencies (5)

coq-hierarchy-builder (>= "1.7.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.2.0" & < "2.5~") | (= "dev")
coq-core (>= "9.0" & < "9.1~") | (= "dev")

Used by (2)

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

Conflicts

None

On This Page

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