| namespace Foo | |
| -- The following declaration shadows the builtin parser alias `letDecl` | |
| syntax letDecl := term ">==>" term | |
| syntax "foo!" letDecl : term | |
| macro_rules | |
| | `(foo! $x:term >==> $y) => `($x + $y) | |
| end Foo | |
| -- The following declaration shadows the builtin parser alias `letDecl` | |
| syntax letDecl := term ">=>=>" term | |
| syntax "bla!" letDecl : term | |
| macro_rules | |
| | `(bla! $x:term >=>=> $y) => `($x * $y) | |
| syntax "boo!" Foo.letDecl : term | |
| macro_rules | |
| | `(boo! $x:term >==> $y) => `($x - $y) | |
| theorem ex1 : (foo! 10 >==> 20) = 30 := rfl | |
| theorem ex2 : (bla! 10 >=>=> 20) = 200 := rfl | |
| theorem ex3 : (boo! 30 >==> 20) = 10 := rfl |