lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Make `trace.Elab.info` a proper message

Open Kha opened this issue 3 years ago • 1 comments

We should move all *Info.format functions to MessageData instead so options like pp.raw and pp.raw.showInfo are heeded correctly.

Kha avatar Oct 03 '22 18:10 Kha

Also it would be nice to be able to click on exprs and such.

digama0 avatar Oct 03 '22 19:10 digama0