Joachim Breitner

I've wanted them myself often as well. However, match compilation is already a very complicated beast and has to worry about verification, completeness checking, equation generation with correct overlapping conditions...

Do you miss them only when doing plain programming, or also when you write functions that you want to verify?

This is since #10271 Not sure if that's a bug in the code: the class determines the signature of the methods, so I cannot drop the arguments here. Or is...

Ah, now I see the discusion on zulip. > I see in this example we previously had > ``` > -- This is relying on an automatically generated instance name,...

Or is there a way to make the definition pass the linter? Use an underscore somewhere?

Looking at the linter code, I don’t see a provision for this (e.g. not warning about function arguments with a user name `_`, indicating that the programmer intended to have...

It's always been like that that derived instances have rather naive assumptions. But until recently the implementation function had an inaccessible name, so probably nobody noticed. Changing the implementation should...

Thanks for the report. `match` statements with dependent targets are notorious tricky. A work-around in your case is to use the non-unfolding induction principle: ``` theorem blub {a : Nat}...

Interesting, this works: ``` def bla (a : Nat) (h : 0 < a) : Nat := if h : a ≤ 1 then 0 else (fun (this : 0...

Some attempt at a fix in #10519, but I’m not sure if this is conceptually the right thing to do. (If not then maybe handling prop-valued `let/have` more gracefully would...