package rocq-num-analysis-subset

Overview
Doc

You can search for identifiers within the package.

in-package search v0.2.0

Subsets for numerical analysis in Rocq

Install

Dune Dependency

lipn.univ-paris13.fr Edit opam file Versions (3)

Authors

Maintainers

M

MILC project <milc@inria.fr>

Sources

rocq-num-analysis-2.2.0.tar.gz

sha512=d1996546d967000045e3c58484d6bda8bf4e153f62d6ee42789090c772f0fede197a41b22cfd8253c2729cec515d0bb834d52904d9a38e656858ee7778aac779

Description

This library provides support about subsets, functions, homogeneous binary relations, and finite families. It is based on classical logic. Some complements about logic and natural numbers are also provided.

Published: 13 Mar 2026

Dependencies (6)

coq-mathcomp-classical >= "1.8" & < "1.15~"
coq-mathcomp-ssreflect >= "2.3" & < "2.6~"
rocq-stdlib
rocq-core >= "9.0" & < "9.2~"
coq-stdlib
coq-core >= "8.20" & < "8.21~"

Dev Dependencies

None

Used by (2)

rocq-num-analysis-algebra >= "2.2.0"
rocq-num-analysis-lebesgue >= "2.2.0"

Conflicts