#
ssreflect
Here are 18 public repositories matching this topic...
Lecture notes for a short course on proving/programming in Coq via SSReflect.
-
Updated
Jun 12, 2020 - Coq
Formal proof of the Four Color Theorem
-
Updated
Apr 17, 2020 - Coq
1
amahboubi
commented
Oct 4, 2019
A few lines in the header of topology.v are confusing, specially those which deal with filtered types.
For instance :
- at this line, what does "canonical" mean here? Should it be "
Tmust be afilteredType? - at [this](https://github.com/math-comp/analysis/blob/3edd010fa7b101f4
Open
Update description
1
affeldt-aist
commented
Apr 29, 2020
The github "Description" for finmap says "Finite sets, finite maps, multisets and order". It should maybe be "Finite sets, finite maps, and multisets" now that order is in MathComp.
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
-
Updated
Jun 10, 2020 - Coq
The formal proof of the Odd Order Theorem
-
Updated
Jun 7, 2020 - Coq
Finite sets and maps for Coq with extensional equality
-
Updated
Mar 22, 2020 - Coq
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
-
Updated
May 29, 2020 - Coq
-
Updated
Jul 25, 2019 - Coq
Improve this page
Add a description, image, and links to the ssreflect topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the ssreflect topic, visit your repo's landing page and select "manage topics."
I could not find in the reviewing checklist a note on how to merge.
In particular if the PR has overlays, one has to merge them.