Joachim Breitner

And do the desired definitional equalities still hold, e.g. ``` theorem Nat.add2_eq1 (a b : Nat) : Nat.add2 (a.succ) b = (a.add2 b).succ := rfl ```

Ah, right, wrong argument… I’m surprised it's slower. Do you have an idea why? In the kernel or the elaborator? Are you comparing with “the” `Nat.add` (with reduce_nat support), or...

Thanks for investigating! You turn `set_option smartUnfolding false` off, but that makes your elaborator measurements not representative. I guess normally, with smartUnfolding on, it doesn’t matter which encoding is used...

Closing this in favor of #10606

Thanks for the heads-up! No, I haven't yet. Should the idiom be `rwa [foo]` then, rather than `simp [foo]` (Probably safer anyways if the goal is to unfold once)? Or...

Mildly related: I just leaned that panics are not visible on https://live.lean-lang.org/. I sometimes wonder if panics within commands couldn’t be somehow caught and turned into error, with a location...

Anyways, the panic message here is ``` PANIC at Lean.Elab.Tactic.SolveByElim.parseArgs Lean.Elab.Tactic.SolveByElim:45:11: Unreachable parse of solve_by_elim arguments. ``` and it can be reproduced on current `master`.

@DanielFabian this the idea that I mentioned, and seems to be able to handle the examples in that bug report. I wonder whether a full proof search is really needed...

> Iirc, the motive is indeed always simple because it is completely opaque to us That's true for constructing `.below`, but when compiling a concrete function (like `T -> True`),...

No worries! I tend to get hazy about details more quickly than that :-)