Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replace
/
.
/
tests
/
lean
/
unknownId.lean
blob: 769fee9fbda30da6c2b55e71383fd7f2fceb4057 [
file
] [
edit
]
macro
"foo"
:
term
=>
`(bla)
#check foo
def f (bla : Nat) : Nat :=
foo
macro "boo" x:term : term => `
(
fun
(
bla
:
Nat
)
=>
$x
+
bla
)
def
g
:
Nat
→
Nat
:=
boo foo