tests/lean/traceClassScopes.lean

import Lean

macro "t" t:interpolatedStr(term) : doElem =>
  `(doElem| Macro.trace[Meta.debug] $t)

macro "tstcmd" : command => do
  t "hello"
  `(example : Nat := 1)

set_option trace.Meta.debug true in
tstcmd

open Lean Meta

macro "r" r:interpolatedStr(term) : doElem =>
  `(doElem| trace[Meta.debug] $r)

set_option trace.Meta.debug true in
#eval show MetaM _ from do r "world"