search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.88k stars 329 forks source link

fix: make erased names in `simp` clickable #4176

Closed nomeata closed 2 weeks ago

nomeata commented 2 weeks ago

as usually, just a matter of using the WithInfo variant.

Also simplifying the code a bit, it seems we can use realizeGlobalConstNoOverloadWithInfo here.

(It's somehwatdubious API design that of all the functions in the {resolve/realise}GlobalConst{NoOverload,}{WithInfo,} family the one with the longest name is the one that should be used unless one has a reason to use another one.)

Fixes: #4174

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):