Alternative Coq standard library std++
This project contains an extended "Standard Library" for Coq called coq-std++. The key features are:
Great number of definitions and lemmas for common data structures such as lists, finite maps, finite sets, and finite multisets.
Type classes for common notations (like ∅, ∪, and Haskell-style monad notations) so that these can be overloaded for different data structures.
It uses type classes to keep track of common properties of types, like it having decidable equality or being countable or finite.
Most data structures are represented in canonical ways so that Leibniz equality can be used as much as possible (for example, for maps we have m1 = m2 iff ∀ i, m1 !! i = m2 !! i). On top of that, the library provides setoid instances for most types and operations.
Various tactics for common tasks, like an ssreflect inspired done tactic for finishing trivial goals, a simple breadth-first solver naive_solver, an equality simplifier simplify_eq, a solver solve_proper for proving compatibility of functions with respect to relations, and a solver set_solver for goals involving set operations.
The library is dependency- and axiom-free.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/7m1m3c2vrpqjr47q60gmqrwh07549g6r-coq-stdpp-1.5.0.drv | ||
| powerpc64le-linux | /gnu/store/1h6jip9z1s54g14d7jnipa7glfskj5ba-coq-stdpp-1.5.0.drv | ||
| mips64el-linux | /gnu/store/6a1xlsd5gfgfw5w76a3yzbsrrv5ir5wh-coq-stdpp-1.5.0.drv | ||
| i686-linux | /gnu/store/bflcd02dqm2lnajprbm9fvjjv8gginaz-coq-stdpp-1.5.0.drv | ||
| i586-gnu | /gnu/store/zkzd65n4zqxhxf9vxvs4izn9pglm9zai-coq-stdpp-1.5.0.drv | ||
| armhf-linux | /gnu/store/wxwb39s2j5h523g9snlxy23lglf9b3jy-coq-stdpp-1.5.0.drv | ||
| aarch64-linux | /gnu/store/lj9b9c7ld54g79akzpyi27d2c6gax4ri-coq-stdpp-1.5.0.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||