Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
secVarBug.lean
blob: f25b33f5b9c682b194d45754cc8151c0222e8a25 [
file
] [
edit
]
variable
{α}
[
ToString
α]
(
n
:
Nat
)
local
macro
"foo"
:
term
=>
`(n)
def f :=
foo
#check f 10
