diff --git a/config.json b/config.json
index 07f848e..9b47b9c 100644
--- a/config.json
+++ b/config.json
@@ -642,6 +642,14 @@
         "prerequisites": [],
         "difficulty": 7
       },
+      {
+        "slug": "zipper",
+        "name": "Zipper",
+        "uuid": "f7bdcd13-7231-4895-a1f8-2f22838a6738",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 7
+      },
       {
         "slug": "all-your-base",
         "name": "All Your Base",
diff --git a/exercises/practice/difference-of-squares/.approaches/config.json b/exercises/practice/difference-of-squares/.approaches/config.json
index 650d318..9a043ac 100644
--- a/exercises/practice/difference-of-squares/.approaches/config.json
+++ b/exercises/practice/difference-of-squares/.approaches/config.json
@@ -1,7 +1,8 @@
 {
   "introduction": {
-    "authors": ["oxe-i"],
-    "contributors": []
+    "authors": [
+      "oxe-i"
+    ]
   },
   "approaches": [
     {
diff --git a/exercises/practice/zipper/.docs/instructions.md b/exercises/practice/zipper/.docs/instructions.md
new file mode 100644
index 0000000..5445db0
--- /dev/null
+++ b/exercises/practice/zipper/.docs/instructions.md
@@ -0,0 +1,27 @@
+# Instructions
+
+Creating a zipper for a binary tree.
+
+[Zippers][zipper] are a purely functional way of navigating within a data structure and manipulating it.
+They essentially contain a data structure and a pointer into that data structure (called the focus).
+
+For example given a rose tree (where each node contains a value and a list of child nodes) a zipper might support these operations:
+
+- `from_tree` (get a zipper out of a rose tree, the focus is on the root node)
+- `to_tree` (get the rose tree out of the zipper)
+- `value` (get the value of the focus node)
+- `prev` (move the focus to the previous child of the same parent,
+  returns a new zipper)
+- `next` (move the focus to the next child of the same parent, returns a
+  new zipper)
+- `up` (move the focus to the parent, returns a new zipper)
+- `set_value` (set the value of the focus node, returns a new zipper)
+- `insert_before` (insert a new subtree before the focus node, it
+  becomes the `prev` of the focus node, returns a new zipper)
+- `insert_after` (insert a new subtree after the focus node, it becomes
+  the `next` of the focus node, returns a new zipper)
+- `delete` (removes the focus node and all subtrees, focus moves to the
+  `next` node if possible otherwise to the `prev` node if possible,
+  otherwise to the parent node, returns a new zipper)
+
+[zipper]: https://en.wikipedia.org/wiki/Zipper_%28data_structure%29
diff --git a/exercises/practice/zipper/.meta/Example.lean b/exercises/practice/zipper/.meta/Example.lean
new file mode 100644
index 0000000..4e9beb7
--- /dev/null
+++ b/exercises/practice/zipper/.meta/Example.lean
@@ -0,0 +1,65 @@
+namespace Zipper
+
+inductive BinTree (α : Type) where
+  | nil  : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
+  deriving BEq, Repr, Inhabited
+
+inductive Crumb (α : Type) where
+  | leftOf  : α → BinTree α → Crumb α
+  | rightOf : α → BinTree α → Crumb α
+  deriving BEq, Repr
+
+structure Zipper (α : Type) where
+  focus  : BinTree α
+  crumbs : List (Crumb α)
+  deriving BEq, Repr
+
+def fromTree (tree : BinTree α) : Zipper α :=
+  { focus := tree, crumbs := [] }
+
+def Zipper.toTree : Zipper α → BinTree α
+  | { focus, crumbs := [] } => focus
+  | { focus, crumbs := .leftOf v r :: cs } =>
+    Zipper.toTree { focus := .node v focus r, crumbs := cs }
+  | { focus, crumbs := .rightOf v l :: cs } =>
+    Zipper.toTree { focus := .node v l focus, crumbs := cs }
+
+def Zipper.value : Zipper α → Option α
+  | { focus := .nil, .. } => none
+  | { focus := .node v _ _, .. } => some v
+
+def Zipper.left : Zipper α → Option (Zipper α)
+  | { focus := .nil, .. } => none
+  | { focus := .node v l r, crumbs } =>
+    match l with
+    | .nil => none
+    | _    => some { focus := l, crumbs := .leftOf v r :: crumbs }
+
+def Zipper.right : Zipper α → Option (Zipper α)
+  | { focus := .nil, .. } => none
+  | { focus := .node v l r, crumbs } =>
+    match r with
+    | .nil => none
+    | _    => some { focus := r, crumbs := .rightOf v l :: crumbs }
+
+def Zipper.up : Zipper α → Option (Zipper α)
+  | { crumbs := [], .. } => none
+  | { focus, crumbs := .leftOf v r :: cs } =>
+    some { focus := .node v focus r, crumbs := cs }
+  | { focus, crumbs := .rightOf v l :: cs } =>
+    some { focus := .node v l focus, crumbs := cs }
+
+def Zipper.setValue (val : α) : Zipper α → Zipper α
+  | { focus := .nil, crumbs } => { focus := .nil, crumbs }
+  | { focus := .node _ l r, crumbs } => { focus := .node val l r, crumbs }
+
+def Zipper.setLeft (tree : BinTree α) : Zipper α → Zipper α
+  | { focus := .nil, crumbs } => { focus := .nil, crumbs }
+  | { focus := .node v _ r, crumbs } => { focus := .node v tree r, crumbs }
+
+def Zipper.setRight (tree : BinTree α) : Zipper α → Zipper α
+  | { focus := .nil, crumbs } => { focus := .nil, crumbs }
+  | { focus := .node v l _, crumbs } => { focus := .node v l tree, crumbs }
+
+end Zipper
diff --git a/exercises/practice/zipper/.meta/config.json b/exercises/practice/zipper/.meta/config.json
new file mode 100644
index 0000000..3f00720
--- /dev/null
+++ b/exercises/practice/zipper/.meta/config.json
@@ -0,0 +1,18 @@
+{
+  "authors": [
+    "jojo8356"
+  ],
+  "files": {
+    "solution": [
+      "Zipper.lean"
+    ],
+    "test": [
+      "ZipperTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Creating a zipper for a binary tree.",
+  "source": "https://en.wikipedia.org/wiki/Zipper_%28data_structure%29"
+}
diff --git a/exercises/practice/zipper/.meta/extra.json b/exercises/practice/zipper/.meta/extra.json
new file mode 100644
index 0000000..6eea4f5
--- /dev/null
+++ b/exercises/practice/zipper/.meta/extra.json
@@ -0,0 +1,135 @@
+{
+  "exercise": "zipper",
+  "comments": [
+    "Extra test cases for the Lean track to test polymorphic tree support."
+  ],
+  "cases": [
+    {
+      "description": "string tree: data is retained",
+      "property": "expectedValue",
+      "input": {
+        "initialTree": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        },
+        "operations": [
+          {
+            "operation": "to_tree"
+          }
+        ]
+      },
+      "expected": {
+        "type": "tree",
+        "value": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        }
+      }
+    },
+    {
+      "description": "string tree: left, right and value",
+      "property": "expectedValue",
+      "input": {
+        "initialTree": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        },
+        "operations": [
+          { "operation": "left" },
+          { "operation": "right" },
+          { "operation": "value" }
+        ]
+      },
+      "expected": {
+        "type": "string",
+        "value": "c"
+      }
+    },
+    {
+      "description": "string tree: set_value",
+      "property": "expectedValue",
+      "input": {
+        "initialTree": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        },
+        "operations": [
+          { "operation": "left" },
+          { "operation": "set_value", "item": "x" }
+        ]
+      },
+      "expected": {
+        "type": "tree",
+        "value": {
+          "value": "a",
+          "left": {
+            "value": "x",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        }
+      }
+    }
+  ]
+}
diff --git a/exercises/practice/zipper/.meta/tests.toml b/exercises/practice/zipper/.meta/tests.toml
new file mode 100644
index 0000000..e93932b
--- /dev/null
+++ b/exercises/practice/zipper/.meta/tests.toml
@@ -0,0 +1,52 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[771c652e-0754-4ef0-945c-0675d12ef1f5]
+description = "data is retained"
+
+[d7dcbb92-47fc-4d01-b81a-df3353bc09ff]
+description = "left, right and value"
+
+[613d8286-b05c-4453-b205-e6f9c5966339]
+description = "dead end"
+
+[dda31af7-1c68-4e29-933a-c9d198d94284]
+description = "tree from deep focus"
+
+[1e3072a6-f85b-430b-b014-cdb4087e3577]
+description = "traversing up from top"
+
+[b8505f6a-aed4-4c2e-824f-a0ed8570d74b]
+description = "left, right, and up"
+
+[b9aa8d54-07b7-4bfd-ab6b-7ff7f35930b6]
+description = "test ability to descend multiple levels and return"
+
+[47df1a27-b709-496e-b381-63a03b82ea5f]
+description = "set_value"
+
+[16a1f1a8-dbed-456d-95ac-1cbb6093e0ab]
+description = "set_value after traversing up"
+
+[535a91af-a02e-49cd-8d2c-ecb6e4647174]
+description = "set_left with leaf"
+
+[b3f60c4b-a788-4ffd-be5d-1e69aee61de3]
+description = "set_right with null"
+
+[e91c221d-7b90-4604-b4ec-46638a673a12]
+description = "set_right with subtree"
+
+[c246be85-6648-4e9c-866f-b08cd495149a]
+description = "set_value on deep focus"
+
+[47aa85a0-5240-48a4-9f42-e2ac636710ea]
+description = "different paths to same zipper"
diff --git a/exercises/practice/zipper/Zipper.lean b/exercises/practice/zipper/Zipper.lean
new file mode 100644
index 0000000..17aad02
--- /dev/null
+++ b/exercises/practice/zipper/Zipper.lean
@@ -0,0 +1,23 @@
+namespace Zipper
+
+/-
+  You should define:
+
+  1. A `BinTree` type representing a binary tree where each node
+     has a value, a left subtree, and a right subtree.
+
+  2. A `Zipper` type that allows navigating within a binary tree.
+
+  3. The following functions:
+     - `fromTree`  : Create a zipper focused on the root of a tree.
+     - `toTree`    : Reconstruct the full tree from a zipper.
+     - `value`     : Get the value of the focused node.
+     - `left`      : Move focus to the left child (returns Option).
+     - `right`     : Move focus to the right child (returns Option).
+     - `up`        : Move focus to the parent (returns Option).
+     - `setValue`  : Set the value of the focused node.
+     - `setLeft`   : Set the left subtree of the focused node.
+     - `setRight`  : Set the right subtree of the focused node.
+-/
+
+end Zipper
diff --git a/exercises/practice/zipper/ZipperTest.lean b/exercises/practice/zipper/ZipperTest.lean
new file mode 100644
index 0000000..517129d
--- /dev/null
+++ b/exercises/practice/zipper/ZipperTest.lean
@@ -0,0 +1,194 @@
+import LeanTest
+import Zipper
+
+open LeanTest
+open Zipper
+
+instance : HAppend AssertionResult AssertionResult AssertionResult where
+    hAppend
+        | .success, .success => .success
+        | .failure msg, _    => .failure msg
+        | _, .failure msg    => .failure msg
+
+def initialTree : BinTree Int :=
+  .node 1
+    (.node 2
+      .nil
+      (.node 3 .nil .nil))
+    (.node 4 .nil .nil)
+
+def zipperTests : TestSuite :=
+  (TestSuite.empty "Zipper")
+    |>.addTest "data is retained" (do
+      let zipper := fromTree initialTree
+      let tree := zipper.toTree
+      return assertEqual initialTree tree)
+    |>.addTest "left, right and value" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.right
+        >>= Zipper.value
+      return assertEqual (some 3) result)
+    |>.addTest "dead end" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.left
+      return assertEqual (none : Option (Zipper Int)) result)
+    |>.addTest "tree from deep focus" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.right
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual initialTree z.toTree)
+    |>.addTest "traversing up from top" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.up
+      return assertEqual (none : Option (Zipper Int)) result)
+    |>.addTest "left, right, and up" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.up
+        >>= Zipper.right
+        >>= Zipper.up
+        >>= Zipper.left
+        >>= Zipper.right
+        >>= Zipper.value
+      return assertEqual (some 3) result)
+    |>.addTest "test ability to descend multiple levels and return" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.right
+        >>= Zipper.up
+        >>= Zipper.up
+        >>= Zipper.value
+      return assertEqual (some 1) result)
+    |>.addTest "set_value" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        |>.map (Zipper.setValue 5)
+      let expected : BinTree Int :=
+        .node 1
+          (.node 5
+            .nil
+            (.node 3 .nil .nil))
+          (.node 4 .nil .nil)
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual expected z.toTree)
+    |>.addTest "set_value after traversing up" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.right
+        >>= Zipper.up
+        |>.map (Zipper.setValue 5)
+      let expected : BinTree Int :=
+        .node 1
+          (.node 5
+            .nil
+            (.node 3 .nil .nil))
+          (.node 4 .nil .nil)
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual expected z.toTree)
+    |>.addTest "set_left with leaf" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        |>.map (Zipper.setLeft (.node 5 .nil .nil))
+      let expected : BinTree Int :=
+        .node 1
+          (.node 2
+            (.node 5 .nil .nil)
+            (.node 3 .nil .nil))
+          (.node 4 .nil .nil)
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual expected z.toTree)
+    |>.addTest "set_right with null" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        |>.map (Zipper.setRight .nil)
+      let expected : BinTree Int :=
+        .node 1
+          (.node 2
+            .nil
+            .nil)
+          (.node 4 .nil .nil)
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual expected z.toTree)
+    |>.addTest "set_right with subtree" (do
+      let modified := (fromTree initialTree).setRight
+        (.node 6
+          (.node 7 .nil .nil)
+          (.node 8 .nil .nil))
+      let expected : BinTree Int :=
+        .node 1
+          (.node 2
+            .nil
+            (.node 3 .nil .nil))
+          (.node 6
+            (.node 7 .nil .nil)
+            (.node 8 .nil .nil))
+      return assertEqual expected modified.toTree)
+    |>.addTest "set_value on deep focus" (do
+      let result := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.right
+        |>.map (Zipper.setValue 5)
+      let expected : BinTree Int :=
+        .node 1
+          (.node 2
+            .nil
+            (.node 5 .nil .nil))
+          (.node 4 .nil .nil)
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual expected z.toTree)
+    |>.addTest "different paths to same zipper" (do
+      let path1 := (some (fromTree initialTree))
+        >>= Zipper.left
+        >>= Zipper.up
+        >>= Zipper.right
+      let path2 := (some (fromTree initialTree))
+        >>= Zipper.right
+      match path1, path2 with
+      | some z1, some z2 => return assertEqual z1.toTree z2.toTree
+      | none, _ => return .failure "path1 returned none"
+      | _, none => return .failure "path2 returned none")
+    -- Extra test cases for String type
+    |>.addTest "string tree: data is retained" (do
+      let tree : BinTree String :=
+        .node "a"
+          (.node "b" .nil (.node "c" .nil .nil))
+          (.node "d" .nil .nil)
+      let zipper := fromTree tree
+      return assertEqual tree zipper.toTree)
+    |>.addTest "string tree: left, right and value" (do
+      let tree : BinTree String :=
+        .node "a"
+          (.node "b" .nil (.node "c" .nil .nil))
+          (.node "d" .nil .nil)
+      let result := (some (fromTree tree))
+        >>= Zipper.left
+        >>= Zipper.right
+        >>= Zipper.value
+      return assertEqual (some "c") result)
+    |>.addTest "string tree: set_value" (do
+      let tree : BinTree String :=
+        .node "a"
+          (.node "b" .nil (.node "c" .nil .nil))
+          (.node "d" .nil .nil)
+      let result := (some (fromTree tree))
+        >>= Zipper.left
+        |>.map (Zipper.setValue "x")
+      let expected : BinTree String :=
+        .node "a"
+          (.node "x" .nil (.node "c" .nil .nil))
+          (.node "d" .nil .nil)
+      match result with
+      | none => return .failure "Expected a zipper but got none"
+      | some z => return assertEqual expected z.toTree)
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [zipperTests]
diff --git a/exercises/practice/zipper/lakefile.toml b/exercises/practice/zipper/lakefile.toml
new file mode 100644
index 0000000..668c8e2
--- /dev/null
+++ b/exercises/practice/zipper/lakefile.toml
@@ -0,0 +1,15 @@
+name = "zipper"
+version = "0.1.0"
+defaultTargets = ["ZipperTest"]
+testDriver = "ZipperTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Zipper"
+
+[[lean_exe]]
+name = "ZipperTest"
+root = "ZipperTest"
diff --git a/exercises/practice/zipper/lean-toolchain b/exercises/practice/zipper/lean-toolchain
new file mode 100644
index 0000000..370b26d
--- /dev/null
+++ b/exercises/practice/zipper/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2
diff --git a/exercises/practice/zipper/vendor/LeanTest/LeanTest.lean b/exercises/practice/zipper/vendor/LeanTest/LeanTest.lean
new file mode 100644
index 0000000..012ba20
--- /dev/null
+++ b/exercises/practice/zipper/vendor/LeanTest/LeanTest.lean
@@ -0,0 +1,4 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test
diff --git a/exercises/practice/zipper/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/zipper/vendor/LeanTest/LeanTest/Assertions.lean
new file mode 100644
index 0000000..60e4ad8
--- /dev/null
+++ b/exercises/practice/zipper/vendor/LeanTest/LeanTest/Assertions.lean
@@ -0,0 +1,166 @@
+/-
+Assertion functions for unit testing.
+-/
+
+namespace LeanTest
+
+/-- Result of a test assertion -/
+inductive AssertionResult where
+  | success : AssertionResult
+  | failure (message : String) : AssertionResult
+  deriving Repr, BEq
+
+namespace AssertionResult
+
+def isSuccess : AssertionResult → Bool
+  | success => true
+  | failure _ => false
+
+def getMessage : AssertionResult → String
+  | success => "Assertion passed"
+  | failure msg => msg
+
+end AssertionResult
+
+/-- Assert that a boolean condition is true -/
+def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult :=
+  if condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that two values are equal -/
+def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected == actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected: {repr expected}\nActual: {repr actual}"
+    else
+      s!"{message}\nExpected: {repr expected}\nActual: {repr actual}"
+    .failure msg
+
+/-- Assert that two values are not equal -/
+def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected != actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected values to be different, but both were: {repr expected}"
+    else
+      s!"{message}\nExpected values to be different, but both were: {repr expected}"
+    .failure msg
+
+/-- Refute that a boolean condition is true (assert it's false) -/
+def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult :=
+  if !condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that a value is true -/
+def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult :=
+  assert value message
+
+/-- Assert that a value is false -/
+def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult :=
+  refute value message
+
+/-- Assert that an Option is some -/
+def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult :=
+  match opt with
+  | some _ => .success
+  | none => .failure message
+
+/-- Assert that an Option is none -/
+def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult :=
+  match opt with
+  | none => .success
+  | some val =>
+    let msg := if message.isEmpty then
+      s!"Expected None but got Some: {repr val}"
+    else
+      s!"{message}\nExpected None but got Some: {repr val}"
+    .failure msg
+
+/-- Assert that a list is empty -/
+def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult :=
+  match list with
+  | [] => .success
+  | _ =>
+    let msg := if message.isEmpty then
+      s!"Expected empty list but got: {repr list}"
+    else
+      s!"{message}\nExpected empty list but got: {repr list}"
+    .failure msg
+
+/-- Assert that a list contains an element -/
+def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult :=
+  if list.contains element then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected list to contain {repr element}\nList: {repr list}"
+    else
+      s!"{message}\nExpected list to contain {repr element}\nList: {repr list}"
+    .failure msg
+
+/-- Assert that a value is within a range (inclusive) -/
+def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α]
+    (value : α) (min : α) (max : α) (message : String := "") : AssertionResult :=
+  if min ≤ value ∧ value ≤ max then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected {repr value} to be in range [{repr min}, {repr max}]"
+    else
+      s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]"
+    .failure msg
+
+/-- Assert that an Except value is an error -/
+def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .error _ => .success
+  | .ok val =>
+    let msg := if message.isEmpty then
+      s!"Expected error but got Ok: {repr val}"
+    else
+      s!"{message}\nExpected error but got Ok: {repr val}"
+    .failure msg
+
+/-- Assert that an Except value is ok -/
+def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .ok _ => .success
+  | .error err =>
+    let msg := if message.isEmpty then
+      s!"Expected Ok but got error: {repr err}"
+    else
+      s!"{message}\nExpected Ok but got error: {repr err}"
+    .failure msg
+
+/-- Assert that an IO action throws an error -/
+def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    let msg := if message.isEmpty then
+      "Expected IO action to throw an error, but it succeeded"
+    else
+      s!"{message}\nExpected IO action to throw an error, but it succeeded"
+    return .failure msg
+  catch _ =>
+    return .success
+
+/-- Assert that an IO action succeeds (doesn't throw) -/
+def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    return .success
+  catch e =>
+    let msg := if message.isEmpty then
+      s!"Expected IO action to succeed, but it threw: {e}"
+    else
+      s!"{message}\nExpected IO action to succeed, but it threw: {e}"
+    return .failure msg
+
+end LeanTest
diff --git a/exercises/practice/zipper/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/zipper/vendor/LeanTest/LeanTest/Test.lean
new file mode 100644
index 0000000..5ddbae5
--- /dev/null
+++ b/exercises/practice/zipper/vendor/LeanTest/LeanTest/Test.lean
@@ -0,0 +1,130 @@
+/-
+Test case and test suite management.
+-/
+
+import LeanTest.Assertions
+
+namespace LeanTest
+
+/-- A single test case -/
+structure TestCase where
+  description : String
+  test : IO AssertionResult
+  deriving Inhabited
+
+/-- Result of running a test -/
+structure TestResult where
+  description : String
+  result : AssertionResult
+  deriving Repr
+
+/-- A collection of tests (test suite) -/
+structure TestSuite where
+  name : String
+  tests : List TestCase
+  deriving Inhabited
+
+namespace TestSuite
+
+/-- Create an empty test suite -/
+def empty (name : String) : TestSuite :=
+  { name := name, tests := [] }
+
+/-- Add a test to the suite -/
+def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult) : TestSuite :=
+  { suite with tests := suite.tests ++ [{ description := description, test := test }] }
+
+end TestSuite
+
+/-- Test statistics -/
+structure TestStats where
+  total : Nat
+  passed : Nat
+  failed : Nat
+  deriving Repr
+
+namespace TestStats
+
+def empty : TestStats :=
+  { total := 0, passed := 0, failed := 0 }
+
+def addResult (stats : TestStats) (result : AssertionResult) : TestStats :=
+  { total := stats.total + 1
+  , passed := if result.isSuccess then stats.passed + 1 else stats.passed
+  , failed := if result.isSuccess then stats.failed else stats.failed + 1
+  }
+
+end TestStats
+
+/-- ANSI color codes for terminal output -/
+def greenColor : String := "\x1b[32m"
+def redColor : String := "\x1b[31m"
+def yellowColor : String := "\x1b[33m"
+def resetColor : String := "\x1b[0m"
+def boldColor : String := "\x1b[1m"
+
+/-- Run a single test and print the result -/
+def runTest (testCase : TestCase) : IO TestResult := do
+  let result ← testCase.test
+  match result with
+  | .success =>
+    IO.println s!"  {greenColor}✓{resetColor} {testCase.description}"
+  | .failure msg =>
+    IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
+    IO.println s!"    {redColor}{msg}{resetColor}"
+  return { description := testCase.description, result := result }
+
+/-- Run all tests in a test suite -/
+def runTestSuite (suite : TestSuite) : IO TestStats := do
+  IO.println s!"\n{boldColor}{suite.name}{resetColor}"
+  let mut stats := TestStats.empty
+
+  for testCase in suite.tests do
+    let result ← runTest testCase
+    stats := stats.addResult result.result
+
+  return stats
+
+/-- Print test summary -/
+def printSummary (stats : TestStats) : IO Unit := do
+  IO.println ""
+  IO.println s!"{boldColor}Test Summary:{resetColor}"
+  IO.println s!"  Total:  {stats.total}"
+  IO.println s!"  {greenColor}Passed: {stats.passed}{resetColor}"
+
+  if stats.failed > 0 then
+    IO.println s!"  {redColor}Failed: {stats.failed}{resetColor}"
+    IO.println s!"\n{redColor}FAILED{resetColor}"
+  else
+    IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}"
+
+/-- Run multiple test suites -/
+def runTestSuites (suites : List TestSuite) : IO Unit := do
+  let mut totalStats := TestStats.empty
+
+  for suite in suites do
+    let stats ← runTestSuite suite
+    totalStats := {
+      total := totalStats.total + stats.total,
+      passed := totalStats.passed + stats.passed,
+      failed := totalStats.failed + stats.failed
+    }
+
+  printSummary totalStats
+
+/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed) -/
+def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do
+  let mut totalStats := TestStats.empty
+
+  for suite in suites do
+    let stats ← runTestSuite suite
+    totalStats := {
+      total := totalStats.total + stats.total,
+      passed := totalStats.passed + stats.passed,
+      failed := totalStats.failed + stats.failed
+    }
+
+  printSummary totalStats
+  return if totalStats.failed > 0 then 1 else 0
+
+end LeanTest
diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean
index 44e01eb..1a801ed 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -85,6 +85,7 @@ import Generator.AnagramGenerator
 import Generator.BobGenerator
 import Generator.MatchingBracketsGenerator
 import Generator.ReverseStringGenerator
+import Generator.ZipperGenerator
 
 import Std
 import Lean.Data.Json
@@ -183,7 +184,8 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod
     ("Anagram", (AnagramGenerator.genIntro, AnagramGenerator.genTestCase, AnagramGenerator.genEnd)),
     ("Bob", (BobGenerator.genIntro, BobGenerator.genTestCase, BobGenerator.genEnd)),
     ("MatchingBrackets", (MatchingBracketsGenerator.genIntro, MatchingBracketsGenerator.genTestCase, MatchingBracketsGenerator.genEnd)),
-    ("ReverseString", (ReverseStringGenerator.genIntro, ReverseStringGenerator.genTestCase, ReverseStringGenerator.genEnd))
+    ("ReverseString", (ReverseStringGenerator.genIntro, ReverseStringGenerator.genTestCase, ReverseStringGenerator.genEnd)),
+    ("Zipper", (ZipperGenerator.genIntro, ZipperGenerator.genTestCase, ZipperGenerator.genEnd))
   ]
 
 end Generator
diff --git a/generators/Generator/Generator/ZipperGenerator.lean b/generators/Generator/Generator/ZipperGenerator.lean
new file mode 100644
index 0000000..820102c
--- /dev/null
+++ b/generators/Generator/Generator/ZipperGenerator.lean
@@ -0,0 +1,163 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace ZipperGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+open {exercise}
+
+{concatAsserts}
+
+def initialTree : BinTree Int :=
+  .node 1
+    (.node 2
+      .nil
+      (.node 3 .nil .nil))
+    (.node 4 .nil .nil)
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+partial def serializeTree (json : Json) : String :=
+  if json.isNull then ".nil"
+  else
+    let v := s!"{json.getObjValD "value"}"
+    let l := serializeTree (json.getObjValD "left")
+    let r := serializeTree (json.getObjValD "right")
+    if l == ".nil" && r == ".nil" then
+      s!"(.node {v} .nil .nil)"
+    else
+      s!"(.node {v} {l} {r})"
+
+def serializeOp (op : Json) : String × Option String :=
+  let name := op.getObjValD "operation" |>.compress |> toLiteral
+  let leanName := match name with
+    | "to_tree" => "toTree"
+    | "set_value" => "setValue"
+    | "set_left" => "setLeft"
+    | "set_right" => "setRight"
+    | other => other
+  match op.getObjVal? "item" with
+  | .ok item =>
+    if item.isNull then
+      (leanName, some ".nil")
+    else match item.getInt? with
+      | .ok n => (leanName, some (intLiteral n))
+      | .error _ => (leanName, some (serializeTree item))
+  | .error _ => (leanName, none)
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let property := getFunName (case.get! "property")
+  let operations := input.getObjValD "operations" |>.getArr? |> getOk
+  match property with
+  | "expectedValue" =>
+    let expectedType := expected.getObjValD "type" |>.compress |> toLiteral
+    let expectedValue := expected.getObjValD "value"
+    let ops := operations.map serializeOp |>.toList
+    match expectedType with
+    | "tree" =>
+      let tree := serializeTree expectedValue
+      let opChain := ops.map fun (name, arg) =>
+        match arg with
+        | some a => s!"{indent}|> Option.map ({exercise}.{name} {a})"
+        | none =>
+          if name == "toTree" then s!"{indent}|> Option.map {exercise}.toTree"
+          else s!"{indent}|> Option.bind {exercise}.{name}"
+      -- First op applied directly to zipper
+      let firstOp := ops.head!
+      let restOps := ops.tail!
+      let firstLine := match firstOp with
+        | (name, some a) =>
+          if name == "toTree" then s!"let result := (fromTree initialTree).toTree"
+          else s!"let result := ({exercise}.{name} {a} (fromTree initialTree))"
+        | (name, none) =>
+          if name == "toTree" then s!"let result := (fromTree initialTree).toTree"
+          else s!"let result := (fromTree initialTree).{name}"
+      if restOps.isEmpty then
+        s!"
+    |>.addTest {description} (do
+      {firstLine}
+      return assertEqual {tree} result)"
+      else
+        let chainLines := restOps.map fun (name, arg) =>
+          match arg with
+          | some a => s!"        |> Option.map ({exercise}.{name} {a})"
+          | none =>
+            if name == "toTree" then s!"        |> Option.map {exercise}.toTree"
+            else s!"        |> Option.bind {exercise}.{name}"
+        let chain := String.intercalate "\n" chainLines
+        if expectedType == "tree" then
+          s!"
+    |>.addTest {description} (do
+      let result := (fromTree initialTree).{(ops.head!).1}
+{chain}
+      match result with
+      | none => return .failure \"Expected a tree but got none\"
+      | some t => return assertEqual {tree} t)"
+        else ""
+    | "int" =>
+      let v := intLiteral (getOk expectedValue.getInt?)
+      let chainOps := ops.map fun (name, arg) =>
+        match arg with
+        | some a => s!"        |> Option.map ({exercise}.{name} {a})"
+        | none =>
+          if name == "value" then s!"        |> Option.bind {exercise}.{name}"
+          else s!"        |> Option.bind {exercise}.{name}"
+      let chain := String.intercalate "\n" chainOps
+      s!"
+    |>.addTest {description} (do
+      let result := some (fromTree initialTree)
+{chain}
+      return assertEqual (some {v}) result)"
+    | "zipper" =>
+      if expectedValue.isNull then
+        let chainOps := ops.map fun (name, _arg) =>
+          s!"        |> Option.bind {exercise}.{name}"
+        let chain := String.intercalate "\n" chainOps
+        s!"
+    |>.addTest {description} (do
+      let result := some (fromTree initialTree)
+{chain}
+      return assertEqual none result)"
+      else ""
+    | _ => ""
+  | "sameResultFromOperations" =>
+    let ops1 := operations.map serializeOp |>.toList
+    let expectedOps := expected.getObjValD "operations" |>.getArr? |> getOk
+    let ops2 := expectedOps.map serializeOp |>.toList
+    let chain1 := ops1.map fun (name, _arg) =>
+      s!"        |> Option.bind {exercise}.{name}"
+    let chain2 := ops2.map fun (name, _arg) =>
+      s!"        |> Option.bind {exercise}.{name}"
+    s!"
+    |>.addTest {description} (do
+      let path1 := some (fromTree initialTree)
+{String.intercalate "\n" chain1}
+      let path2 := some (fromTree initialTree)
+{String.intercalate "\n" chain2}
+      match path1, path2 with
+      | some z1, some z2 => return assertEqual z1.toTree z2.toTree
+      | none, _ => return .failure \"path1 returned none\"
+      | _, none => return .failure \"path2 returned none\")"
+  | _ => ""
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end ZipperGenerator