Qiu233 · March 14, 2024 21:02 · Mar 14, 2024
diff --git a/LamTerm.lean b/LamTerm.lean
@@ -0,0 +1,31 @@
+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)]