| -- | |
| def A.x : Nat := 10 | |
| def B.x : String := "hello" | |
| def f (a : Nat) := a + 1 | |
| def g (s : String) := s ++ " world" | |
| open A | |
| open B | |
| #check f x | |
| #check g x | |
| macro "foo!" x:term : term => `($x + (1:Nat)) | |
| macro "foo!" x:term : term => `(Append.append $x " world") | |
| #check f (foo! 1) | |
| #check g (foo! "hello") | |
| macro "bla!" : term => `((1 : Nat)) | |
| macro "bla!" : term => `("hello world") | |
| #check f bla! | |
| #check g bla! |