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...
#### Description of the problem I just accidentally discovered this issue (see the code), and it asked me to report. ``` Fact uip_nat {n : nat} (e : n =...
Update syntax and descriptions in the tactics chapter. Done: ~~Still tons of updating I have to do, but perhaps you would be willing to suggest how to reorganize the "Semantics"...
This has been a long-requested feature that we need to implement it properly for users; after a bit of discussion with Ali we decided to go ahead. For now, the...
#### Description of the problem Compiling this program makes `coqc` go into an infinite loop. Note that there is a "bug" in the program because I commented out `(Equivalence F)....
#### Description of the problem As mentioned in QuickChick/QuickChick#294, QuickChick extracts Z to either integer or big integer based on the underlying Coq version, because the ideal extraction module only...
Strict mode means we fail when we cannot locate a file. This is an experiment before implementing `-modules`. Relevant OCaml issue is https://github.com/ocaml/ocaml/issues/8625
Coq should provide a make target that builds only documentation, so that we can offer a `coq-doc` opam package. Also see https://github.com/coq/coq/issues/4855.
Can it be fixed? ``` /usr/bin/make DESTDIR=//debian/tmp install make[2]: Entering directory '/' To install Coq using dune, use 'dune build -p P && dune install P' where P is any...
#### Description of the problem ssreflect tactics often fail for lemmas declared without `Set Implicit Arguments`; the typical workaround is to replace `lemma` with `lemma _ _ _`, with underscores...
The idea is to warn when KEYWORD and IDENT are parsed and there is no space between them and KEYWORD ends with an ident-character. Eg `*m` infix KEYWORD and input...
