19 lines
366 B
Text
19 lines
366 B
Text
import Lean
|
|
|
|
macro "t" t:interpolatedStr(term) : 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 =>
|
|
`(trace[Meta.debug] $r)
|
|
|
|
set_option trace.Meta.debug true in
|
|
#eval show MetaM _ from do r "world"
|