Pretty printing free variables

Stream: metaprogramming / tactics

[Hanno Becker]

Hi, the metaprogramming book has this example for printing the current goal

elab "custom_assump_0" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    dbg_trace f!"goal type: {goalType}"

example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by
  custom_assump_0
-- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
-- unsolved goals
-- H1 : 1 = 1
-- H2 : 2 = 2
-- ⊢ 2 = 2

When using this on goals with free variables instead, say, example (x y : Nat) (H1 : x = x) (H2 : y = y): y = y, the following is printed:

example (x y : Nat) (H1 : x = x) (H2 : y = y): y = y := by
  custom_assump_0
-- goal type: goal type: Eq.{1} Nat _uniq.24622 _uniq.24622

Is there a way to print user names rather than _uniq.XXX?

[Kim Morrison]

import Lean

open Lean

elab "custom_assump_0" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    logInfo m!"goal type: {goalType}"

example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by
  custom_assump_0

example (x y : Nat) (H1 : x = x) (H2 : y = y): y = y := by
  custom_assump_0

[Kim Morrison]

(Using m! to construct a MessageData, instead of f! to construct a Format. Then we have to change dbg_trace to logInfo to handle the more structured argument.)

[Hanno Becker]

Excellent, thank you for the lightning fast reply :pray: