Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
lean
/
sanitizeMacroScopes.lean
blob: b3735f0351587bff7733a9d422172445c3169f2e [
file
] [
edit
]
macro
"m"
x
:
term
:
term
=>
`(fun x => $x)
set_option trace.Elab.step true in
#check fun x => m x