coq
coq copied to clipboard
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 developme...
- ~~[ ] Added / updated **test-suite**.~~ - [x] Added **changelog**. - ~~[ ] Opened **overlay** pull requests.~~
#### Description of the problem ```coq From Coq Require Import Uint63 List PArray. Open Scope uint63_scope. Open Scope list_scope. Check [| 1; 2 | 0 : int |]. Import ListNotations....
#### Description of the problem ``` $ cat foo.v ``` ```coq Require Import Coq.derive.Derive. Derive foo SuchThat (foo = 1) As foo_eq. Proof. subst foo; reflexivity. Qed. ``` ``` $...
### Is your feature request related to a problem? The current handling of rewrite rules where some of the patterns are function types seems to not only be awkward (while...
~~~coq Set Universe Polymorphism. #[universes(template)] Inductive foo := . (* Template-polymorphism and universe polymorphism are not compatible. *) ~~~ The explicit `universes(template)` should override the option IMO
#### Feature wish It would be nice, if `coqc -vok` would continue checking the next proof, if one proof fails. One could then easily produce a list of all proofs...
Instead of performing useless work and returning data that was not used in most cases, we reorder the branches to make the code cleaner.
Now we really have `Pattern.constr_pattern` for evaluated patterns, and `[`uninstantiated] Pattern.constr_pattern_r` for globalized but not evaluated patterns. Although it seems to turn the `Any -> user_err ?loc (str "Quotations not...
Since we removed the generic constr hint feature, this is now useless. Overlays: - https://github.com/LPCIC/coq-elpi/pull/837 - https://github.com/mattam82/Coq-Equations/pull/657 - https://github.com/mit-plv/fiat/pull/123