arith-with-normal-plus-times.lean

-- example on parsing arith language via macros
inductive Arith: Type :=
   | Mul : Arith -> Arith -> Arith -- e :* f
   | Symbol : String -> Arith -- variable

declare_syntax_cat arith

syntax term : arith -- int for Arith.Int
syntax str : arith -- strings for Arith.Symbol
syntax:70 arith "*" arith : arith -- Arith.Mul

-- auxiliary notation for translating `arith` into `term`
syntax "Arith| " arith : term

macro_rules
  | `(Arith| $s:strLit) => `(Arith.Symbol $s)
  | `(Arith| $x:arith * $y:arith) => `(Arith.Mul (Arith| $x) (Arith| $y))

def foo := (Arith| "x" * "y") -- mul
#print foo

def foo2 := (Arith| ("x" * "y")) -- mul
#print foo2

def foo3 := ((Arith| "x") * "y") -- mul
#print foo3

errors.txt

../code.lean:19:12: error: elaboration function for '«termArith|_»' has not been implemented
  Arith| "x" * "y"
../code.lean:20:7: error: unknown constant 'foo'
../code.lean:22:13: error: elaboration function for '«termArith|_»' has not been implemented
  Arith| ("x" * "y")
../code.lean:23:7: error: unknown constant 'foo2'
../code.lean:25:13: error: failed to synthesize instance
  HMul Arith String ?m.1523
../code.lean:26:7: error: unknown constant 'foo3'