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