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...
This PR clean up some code path in the kernel, ensuring side effects are either there or not there (which was previously checked dynamically). Fix #13324 - https://github.com/maximedenes/vscoq/pull/10
Currently coqidetop doesn’t look for or apply _CoqProject settings directly. Instead, it relies on the IDE to find the _CoqProject file for the running script and to pass the necessary...
#### Description of the problem The vo files produced by `coqc` are often relatively large. For example, the Stdlib binary files on Coq 8.15 and 8.16 are around 100 MB,...
https://github.com/coq/coq/blob/dc01d6d69d5af9f4c95962ae8ed47151fbe8fd1b/theories/Init/Specif.v#L974 It looks like this can be generalized to `Type`. Is there a reason why it is `Set`?
#### Description of the problem Using `unfold` tactic on an opaque term with `at` results in the following error message. ``` Anomaly "Uncaught exception Environ.NotEvaluableConst(1)." Please report at http://coq.inria.fr/bugs/. ```...
~~~coq Universes u v. Constraint u < v. (* or v < u *) Axiom X : Type@{u} = Type@{v}. Lemma foo : forall (P : Type@{u}) (p1 p2 :...
- [x] Added Instance DecidableClass.Decidable_eq_Q : forall (x y : Q), DecidableClass.Decidable (x == y)%Q. - [x] Added Instance DecidableClass.Decidable_le_Q : forall (x y : Q), DecidableClass.Decidable (x
#### Description of the problem The `Coq.Structures.Equalities` library file declares the `~=` notation (in the empty scope) to mean inequivalence according to some equivalence relation: ```` Module Type EqNotation (Import...