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

Authors

Maintainers

R

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

Sources

sha256=ea9cf8653f1e63e01f76393231d048ecd693793ca69a12f28fcc7d43a30e5e46

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: 20 Feb 2025

Dependencies (5)

coq-hierarchy-builder (>= "1.4.0")
coq-mathcomp-finmap (>= "2.0.0")
coq-mathcomp-algebra
coq-mathcomp-fingroup
coq-mathcomp-ssreflect >= "2.1.0" & < "2.4~"

Dev Dependencies (1)

coq (>= "8.19" & < "8.21~") | (= "dev")

Used by (6)

Conflicts

None

On This Page

Description
Dependencies (5)
Dev Dependencies (1)
Used by (6)
Conflicts