Qq error in lean-pr-testing-4096

Stream: mathlib4

[Kim Morrison]

There's a problem in norm_num, using =Q, on the lean-pr-testing-4096 branch, that I'm stumped on. If any Qq afficionados are available to take a look that would be great. It's in Mathlib/Tactic/NormNum/Pow.lean.

(This is hopefully a big performance improvement at lean#4096, so I'd like to get this sorted out.)

[Thomas Murrills]

Hmm, this is weird. If you move the have … =Q … line(s) under the match, it doesn’t complain.

[Kim Morrison]

Thanks!

[Kim Morrison]

That will suffice for me right now. :-)

[Kim Morrison]

Woah, although then adding back in an #adaptation_note explaining the duplication causes it to break again...

[Kim Morrison]

Works outside the def, I guess.

[Thomas Murrills]

Looks like putting a do after the #adaptation_note would be necessary for the inline use! I think maybe because #adaptation_note is a term elaborator, so it changes how things get parsed?

[Thomas Murrills]

I suppose it would make sense to also have "#adaptation_note " (docComment)? : doElem?

[Thomas Murrills]

(Er, I’m assuming you’ll push, seeing as you seemed to be writing the adaptation note; hope I’m inferring correctly!)