Simple lambda calculus representation with macro for Lean4.

LamTerm.lean

import Lean

inductive LamTerm where
| var (n : Nat)
| app (M N : LamTerm)
| abs (M : LamTerm)

instance : ToString LamTerm where
  toString :=
    let rec f := fun t =>
    match t with
    | LamTerm.var x => toString x
    | LamTerm.app M N => "(" ++ f M ++ " " ++ f N ++ ")"
    | LamTerm.abs M => "(λ" ++ " " ++ f M ++ ")"
    f

declare_syntax_cat lambda_term

syntax num : lambda_term
syntax:60 lambda_term:60 lambda_term:61 : lambda_term
syntax "λ" lambda_term : lambda_term
syntax "(" lambda_term ")" : lambda_term
syntax "`[" "λ" "|" lambda_term "]" : term

macro_rules
| `(`[λ| $n:num]) => `(LamTerm.var $n)
| `(`[λ| $M:lambda_term $N:lambda_term]) => `(LamTerm.app `[λ| $M] `[λ| $N])
| `(`[λ| λ $M:lambda_term]) => `(LamTerm.abs `[λ| $M])
| `(`[λ| ($M:lambda_term)]) => `(`[λ| $M])

#eval `[λ| (λ 0 0) (λ 0 0)]