Eric Wieser (Oct 22 2020 at 08:54):
Instead of showing me the full signature, my info boxes when hovering over a lemma name now show:
Provider: jroesch.lean score: 80, compared 'list.prod_range_succ' with 'list.prod_' distance: 0, see localityBonus-setting index: 92, based on sortText: "list.prod_range_succ"
instead of actually showing the signature I care about. Have I toggled a setting by accident?
Bryan Gin-ge Chen (Oct 22 2020 at 08:58):
Eric Wieser (Oct 22 2020 at 09:13):
Thanks - the shortcut is shared with "comment out"!
Last updated: May 16 2021 at 21:11 UTC