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 adds following facts to stdlib: * `pointwise_bounded_dec_ex_dec: (forall x, decidable (P x)) -> (forall x, P x -> x decidable (exists x, P x)`. * `decidable (Nat.divide a...
While working on #17950, I found an incompleteness of `Rtree.inter`, that is a case of two equal recursive trees whose computation of the intersection was raising an `assert false`. The...
This fixes another failure to refolding fixpoints in `simpl`: the refolding mechanism was bypassed for "never simpl" constants used in position of argument of a destructor in tactic "simpl". Example:...
Fixes / closes #???? - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new /...
Fix #18017 Depends on https://github.com/coq/coq/pull/18596
Fixes #17603 I removed Unicode subscript characters from doc directory. They are not shown well in PDF (and HTML on Android). I used :n: to describe subscripts without the characters....
According to the [refman](https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.subst), `subst` preserves the order of hypotheses. However, in the following example, it flips the order of `A` and `B`: ```coq Lemma test(k f: nat)(E: k =...
Fixes / closes #???? - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new /...
