ionathanch/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
OCamlLGPL-2.1
Issues
- 1
`rewrite ?H` is broken
#18 opened by ionathanch - 1
Fixpoints using variables fail to type check
#16 opened by ionathanch - 0
- 4
Recursion via helper function that preserves/reduces size is still rejected by termination checker
#13 opened by fbanados - 0
Preserve sizes in Definitions
#4 opened by ionathanch - 1
- 1
Improve UI for sized typing
#8 opened by ionathanch - 2
- 0
- 3
- 1
Performance issues with test suite
#12 opened by ionathanch - 0
Deduplicate size constraints
#11 opened by ionathanch - 7
- 0
- 1