From 323b87189c3b596562c1f3397d8aa760a8c6df6f Mon Sep 17 00:00:00 2001
From: Bram van den Heuvel <bram.vdh1999@gmail.com>
Date: Mon, 29 Jun 2026 16:44:43 +0200
Subject: [PATCH] Add List constructors & methods

---
 proof.py | 30 +++++++++++++++++++++---------
 1 file changed, 21 insertions(+), 9 deletions(-)

diff --git a/proof.py b/proof.py
index 8013be1..b8f5240 100644
--- a/proof.py
+++ b/proof.py
@@ -106,19 +106,30 @@ def apply_rules() -> dict[str, F]:
             case Const("Bool.Contradiction"):
                 return Truth()
     
+    def __list_isempty(x : Term) -> Term | None:
+        match x:
+            case Const("List.Nil"):
+                return Truth()
+        
+            case App(f=App(f=Const("List.Cons"))):
+                return Contradiction()
+    
+    def __list_length(x : Term) -> Term | None:
+        match x:
+            case Const("List.Nil"):
+                return Zero()
+            
+            case App(f=App(f=Const("List.Cons"), x=head), x=tail):
+                return Succ(A1("List.length", tail))
+
     def __nat_add(x : Term, y : Term) -> Term | None:
         match x:
             case Const("Nat.Zero"):
                 return y
             
             case App(f=Const("Nat.Succ"), x=x_):
-                return Succ(
-                    App(
-                        f=App(Const("Nat.add"), x_),
-                        x=y,
-                    )
-                )
-    
+                return Succ(A2("Nat.add", x_, y))
+
     def __nat_iszero(x : Term) -> Term | None:
         match x:
             case Const("Nat.Zero"):
@@ -126,13 +137,14 @@ def apply_rules() -> dict[str, F]:
             
             case App(f=Const("Nat.Succ")):
                 return Contradiction()
-    
+
     return {
         "Bool.not": F1(__bool_not),
+        "List.isEmpty": F1(__list_isempty),
+        "List.length": F1(__list_length),
         "Nat.add" : F2(__nat_add),
         "Nat.isZero" : F1(__nat_iszero),
     }
-                
 
 def normalize(term : Term) -> Term:
     match term: