Coq-Equations
Coq-Equations copied to clipboard
mattam82
A function definition package for Coq
In the example below (tested with Coq 8.19+Equations 1.3+8.19 and Coq 8.20+Equations 1.3.1+8.20), Equations generates an ill-typed term for the second clause. The example can be made to work by...
The following code fails on Coq 8.20 and Equations 1.3.1. ```coq Equations foo (I : Type) : bool := foo I := true. ``` The error message is `Unable to...
This is a re-filing of https://github.com/mattam82/Coq-Equations/issues/449, which apparently has not actually been fixed yet. The bug is demonstrated by the following proof script: ``` Module Import tactics. Tactic Notation "simplify_eq"...
This looks like a bug: https://coq.zulipchat.com/#narrow/channel/237659-Equations-devs-.26-users/topic/Equations.20vs.20Function/near/486295559
The definition of fvec_to_vec below, is non-idiomatic, but I believe should give better error messages. Coq complains: > Functional induction principle could not be proved automatically, it is left as...
Coming from [this](https://coq.zulipchat.com/#narrow/channel/237659-Equations-devs-.26-users/topic/f_unfold.20obligation.20after.20Defined.20issue) topic on zulip, I've built a smaller example: ``` Equations example {T : Type} (s : seq T) : seq T by wf (seq.size s) lt :=...
