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

Authors

Maintainers

R

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

Sources

analysis-1.12.0.tar.gz

sha256=b8a5c7d7dd8303a148f7e69386d705baf98f5d3426d74d6fa6cdf3c252b2d9b2

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: 07 Jul 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.12.0"

Conflicts

None

On This Page

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