Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
lean
/
414.lean
blob: c9269557b90e609e9fcb715031e1adcc21bc3c3e [
file
] [
edit
]
macro_rules
(
kind
:=
num
)
|
`($n:num) => `
(
"world"
)
#check 2
macro_rules
|
`($n:num) => `
(
"hello"
)
#check 2
macro_rules
(
kind
:=
num
)
|
n
=>
`("boo")
#check 2