Print expression with info

Stream: lean4

[Bhavik Mehta]

Here's a small command I made out of curiosity, which prints the ring normal form of an expression:

import Mathlib

section

open Lean Elab Meta Command Mathlib.Tactic

elab "#ring_nf " e:term : command =>
  Command.runTermElabM fun _ => do
    let e ← Elab.Term.elabTermAndSynthesize e none
    let f ← RingNF.M.run (← IO.mkRef {}) {} (RingNF.rewrite e)
    IO.println s!"{← ppExpr f.expr}"

end

variable {R : Type*} [CommRing R] (a b : R)

#ring_nf (a + b) ^ 4

but in the output, I can't hover over subterms and get useful information. I presume this is because one of ppExpr and IO.println is discarding that information, what should I be using instead?

[Bhavik Mehta]

(I realize #conv ring_nf does the same thing, this is just a toy example since I'm trying to learn)

[Patrick Massot]

I would guess logInfo

[Bhavik Mehta]

Ah! That works, thank you Patrick!

[Bhavik Mehta]

For completeness:

elab "#ring_nf " e:term : command =>
  Command.runTermElabM fun _ => do
    let e ← Elab.Term.elabTermAndSynthesize e none
    let f ← RingNF.M.run (← IO.mkRef {}) {} (RingNF.rewrite e)
    logInfo f.expr

[Jannis Limperg]

More generally, String and Format (which ppExpr produces) are just text. MessageData (which the implicit coercion produces) has the necessary metadata for hovers etc.

[Bhavik Mehta]

Jannis Limperg said:

More generally, String and Format (which ppExpr produces) are just text. MessageData (which the implicit coercion produces) has the necessary metadata for hovers etc.

I'd figured this bit out, but not how to actually display MessageData, logInfo was the exact missing piece for me!