Joachim Breitner
Joachim Breitner
In a way that’s expected – the (actual) goal of `conv` contains a metavariable for the RHS, which depends on the context. One might wonder if `clear` should remove hypothesis...
If you know what you want to rewrite to, maybe use `equals_to` to instantiate the goal, then `clear` and then use omega. (Untested)
I think it’s a separate issue, it says “failed to generate equational theorem for 'popLast'”, not “failed to generate unfold theorem” (which is a later step), so a separate issue...
~~This works now, possibly due to #6901 (will confirm later which nightly unbroke it).~~
Ok, this really seems to work now, at least since Lean 4.23.0
In the interested of pragmaticm, we should probably stick to “overwhelming majority of declarations use” and keep the one with `where`, even if inconsistent with the `def`-with-guards syntax
So here is what’s happening. I generalized this a bit to make it clearer ``` def TTrue (_f : F) := True def F.asdf : (f : F) → TTrue...
Hmm, that seems to be about `mkBelow`, not about about the equation compiler. > this latter proof state is a bit different from what I would've expected. Why is the...
Oh, I like that last idea: perform termination checking and compilation with an *abstract* motive for the function (in all three variants of termination checking). After all, termination checking is...
That's annoying. Does it have to be lazy?