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

Authors

Maintainers

R

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

Sources

analysis-1.14.0.tar.gz

sha256=358afb3f7418fda5462ddbbaa510af4af68bd17a2cbb766dd23ada04e72f880a

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: 12 Nov 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.4.0" & < "2.6~") | (= "dev")
coq-core (>= "9.0" & < "9.1~") | (= "dev")

Used by (5)

Conflicts

None

On This Page

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