Coq-Equations
Coq-Equations copied to clipboard
mattam82
A function definition package for Coq
Vernacular `Derive` conflicts with Rocq [Derive](https://rocq-prover.org/doc/V8.18.0/refman/addendum/miscellaneous-extensions.html) feature. This means that using Derive in stdlib makes Equations build [fail](https://github.com/rocq-prover/stdlib/actions/runs/15656799924/job/44108955927?pr=170#step:12:283). See also: - https://github.com/mattam82/Coq-Equations/pull/645
With @JulesViennotFranca and @fpottier we encountered an instance of code that works fine with Coq 8.19 and Equations 1.3+8.19, but produces an ill-typed term (due to universe issues, it seems)...
Hello! I am trying to define a function by well-founded recursion (using `Equations ... by wf`). The definition involves a `with` node. There is a recursive call inside the `with`...
Avoid having sort quality variables in a non-sort poly context.
We typically track the latest stable `dev` branch in CI to ensure that when there's a point release, all our packages keep working. However, it seems that currently there is...
The regular match pattern elaborator is able to insert constructor coercions in a match pattern when the type of the pattern and the discriminee are known. For example: ```coq Inductive...
As discussed on Zulip, the following example with monadic binders and mutual well-founded recursion fails: ``` From ExtLib Require Export Monads MonadState StateMonad. Require Import Coq.Lists.List. From Equations Require Import...
- depelim should be an alias for dependent elimination? - improve return messages for noconf, depelim, dependent elim
