package coq-mathcomp-finmap

Overview
No Docs

You can search for identifiers within the package.

in-package search v0.2.0

Finite sets, finite maps, finitely supported functions

Install

Dune Dependency

github.com Edit opam file Versions (15)

Authors

Maintainers

C

Cyril Cohen <cyril.cohen@inria.fr>

Sources

2.1.0.tar.gz

sha512=8909143c454c90f8669dcf9232581fee7cbb18bceb5082e1448481fb544709ad9077d29c44931d26a39e1ee78560f28429758c3c24cbaa6dea3942d256f2c008

Description

This library is an extension of mathematical component in order to support finite sets and finite maps on choicetypes (rather that finite types). This includes support for functions with finite support and multisets. The library also contains a generic order and set libary, which will be used to subsume notations for finite sets, eventually.

Published: 17 Jan 2024

Dependencies

None

Dev Dependencies (2)

coq-mathcomp-ssreflect (>= "2.0.0" & < "2.4~") | (= "dev")
coq (>= "8.16" & < "8.21~") | (= "dev")

Used by (6)

Conflicts