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

Authors

Maintainers

M

MILC project <milc@inria.fr>

Sources

rocq-num-analysis-2.1.0.tar.gz

sha512=515ad6799b3e8916beaca37c65a9d25e3f0e1b09d38c44afa8809f41ffcc9e39c92f241afff171d08e0c31bd71724bb3f21f4f4ae3294ffa44828203a468cca8

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: 27 Nov 2025

Dependencies (5)

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

Dev Dependencies

None

Used by (2)

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

Conflicts