finmap

Choice type map library

A Coq library that provides support for finite sets and maps on choice types

Finite sets, finite maps, multisets and generic sets

GitHub

46 stars
16 watching
28 forks
Language: Coq
last commit: 6 months ago
Linked from 2 awesome lists

coqfinite-setsmathcompssreflect

Backlinks from these awesome lists:

Related projects:

Repository Description Stars
math-comp/math-comp A comprehensive repository of formalized mathematical theories based on Coq and SSReflect. 587
thery/mathcomp-extra A collection of reusable mathematical components and algorithms implemented in Coq 5
math-comp/docker-mathcomp Provides Docker images for a Coq proof assistant library 6
coq-community/gaia A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics 28
charguer/tlc A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. 38
math-comp/analysis A comprehensive Coq proof-assistant library for mathematical analysis 206
coq-community/math-classes A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq 162
unimath/unimath Formalizes mathematics using the univalent point of view 961
math-comp/mczify A Coq library that enables the use of Micromega arithmetic solvers for goals stated with Mathematical Components definitions 23
dmxlarchey/kruskal-finite Tools for proving properties about finite types and predicates using proof assistants 0
math-comp/coq-combi Formalises algebraic combinatorics in Coq using symmetric functions and polynomials 36
coq-community/hydra-battles Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. 68
math-comp/multinomials A Coq-based library for manipulating monomials and multivariate polynomials over ring structures 14
coq-community/coqeal A Coq library providing algebraic data structures and algorithms 66