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...
``` $ coqc --config cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you...
**Kind:** cleanup Fixes / closes #15562 This organizes the naming of functions for destructing/constructing abstractions or products wrt contexts around the schemes "{decompose_,strip_,}{lam,prod}{_n,}{_assum,_decls,}{_red,}" and "dest{Lambda,Prod}{_red,}". See #15562 for details. Better...
I'd like an equivalent of Agda's `hiding` when doing [filtered import](https://coq.inria.fr/refman/language/core/modules.html#grammar-token-filtered_import), something like `Import foo(-(id, compose))`, which has the effect of adding everything not in the inner parentheses.
#### Description of the problem Computation gets stuck on `eqb_correct` for native integers. This is a problem in particular when using `Int63.cast`, which blocks reduction. ```coq Require Import Int63. Goal...
Before Dune 2.7, Dune was implicitly adding the `:standard` set of variables to our CC invocation for `kernel/byterun`. This set is `-O2 -fno-strict-aliasing -fwrapv -fPIC`, but after discussion we want...
#### Description of the problem `typeclasses eauto` may fail on a trivial goal, whereas `typeclasses eauto with nocore` succeeds (using stronger unification). ```coq Create HintDb empty. Goal forall (P :...
#### Description of the problem If `typeclasses eauto with core` is being suggested as a replacement for `eauto`, then it should support `using` as well. cc @mattam82 #### Coq Version...
#### Version Tested with coq 8.6 and 8.7 #### Description of the problem As illustrated by the snippet below, in some cases, hints added using `Hint Resolve` seem to not...
#### Description of the problem `congruence` is designed to work on non-dependent terms. However, its obliviousness can lead to unexpected behavior and regressions https://github.com/coq/coq/issues/16140. The example below shows `congruence` both...