From b1c1f386888f2f89c9aeba9a23ab062a89996b46 Mon Sep 17 00:00:00 2001
From: Quinn Dougherty <quinn@for-all.dev>
Date: Tue, 16 Dec 2025 11:14:02 -0500
Subject: [PATCH 1/4] Chore: update Lean to v4.26.0

---
 LSpec/Instances.lean | 2 +-
 LSpec/LSpec.lean     | 2 +-
 lean-toolchain       | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/LSpec/Instances.lean b/LSpec/Instances.lean
index 94ee15c..c1c6398 100644
--- a/LSpec/Instances.lean
+++ b/LSpec/Instances.lean
@@ -56,7 +56,7 @@ instance Nat.Testable_forall_lt
           | none     => s!"Fails on input {b}."
       | .isFailure msg => .isFailure msg
     | .isMaybe msg => .isMaybe msg
-    | .isFalse h msg => .isFalse (λ h' => h λ n hn => h' _ (Nat.le_step hn)) msg
+    | .isFalse h msg => .isFalse (λ h' => h λ n hn => h' _ (Nat.le_succ_of_le hn)) msg
     | .isFailure msg => .isFailure msg
 
 end LSpec
diff --git a/LSpec/LSpec.lean b/LSpec/LSpec.lean
index 3dab516..a425c13 100644
--- a/LSpec/LSpec.lean
+++ b/LSpec/LSpec.lean
@@ -129,7 +129,7 @@ def withExceptError (descr : String) (exc : Except ε α) [ToString α]
 
 /-- A generic runner for `TestSeq` -/
 def TestSeq.run (tSeq : TestSeq) (indent := 0) : Bool × String :=
-  let pad := String.mk $ List.replicate indent ' '
+  let pad := String.ofList $ List.replicate indent ' '
   let rec aux (acc : String) : TestSeq → Bool × String
     | .done => (true, acc)
     | .group d ts n =>
diff --git a/lean-toolchain b/lean-toolchain
index c00a535..e59446d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.26.0

From 023bdaad50e20631e165b418c8ce5434e0a2b6fa Mon Sep 17 00:00:00 2001
From: Quinn Dougherty <quinn@for-all.dev>
Date: Tue, 16 Dec 2025 11:50:33 -0500
Subject: [PATCH 2/4] Chore: update `lean4-nix` flake input

---
 flake.lock | 7 ++++---
 flake.nix  | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/flake.lock b/flake.lock
index 0a5c5f4..6f012ed 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,15 +42,16 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1761368467,
-        "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=",
+        "lastModified": 1765824817,
+        "narHash": "sha256-81IuI/Q/y9QG5gLK4ZKzlHC+mVb2SvbyS71Ro2FmOK8=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "3550873ed1a87d666d633d34921e79abaa4671c1",
+        "rev": "86c3e53196ff3c08049e464821bcbebbb9ee8ba6",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
+        "ref": "manifest/v4.26.0",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 69795e7..363bd77 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.follows = "lean4-nix/nixpkgs";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    lean4-nix.url = "github:lenianiva/lean4-nix/manifest/v4.26.0";
   };
 
   outputs = inputs @ {

From 6643220e1f14e9abafcf25224f5efa42d3df67c7 Mon Sep 17 00:00:00 2001
From: Quinn Dougherty <quinn@for-all.dev>
Date: Tue, 16 Dec 2025 12:00:02 -0500
Subject: [PATCH 3/4] Chore: update flake.nix for new lake2nix syntax

---
 flake.nix | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/flake.nix b/flake.nix
index 363bd77..caf3581 100644
--- a/flake.nix
+++ b/flake.nix
@@ -26,8 +26,10 @@
         pkgs,
         self',
         config,
+        lib,
         ...
-      }: {
+      }: let lake2nix = pkgs.callPackage lean4-nix.lake {};
+        in {
         _module.args.pkgs = import nixpkgs {
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
@@ -35,10 +37,11 @@
 
         # Build the library with `nix build`
         packages.default =
-          ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+          lake2nix.mkPackage {
+            name = "LSpec";
             src = ./.;
             roots = ["LSpec"];
-          }).modRoot;
+          };
 
         devShells.default = pkgs.mkShell {
           packages = with pkgs.lean; [lean-all];

From 98456e0ca6b5853f01dc9d7c75a26f81c9b7881f Mon Sep 17 00:00:00 2001
From: Quinn Dougherty <quinn@for-all.dev>
Date: Tue, 16 Dec 2025 16:15:13 -0500
Subject: [PATCH 4/4] Chore: remove branch from flake input

Now that leni's lean4-nix PR105 was merged in
---
 flake.lock | 5 ++---
 flake.nix  | 4 +---
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/flake.lock b/flake.lock
index 6f012ed..ad7a75d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,16 +42,15 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1765824817,
+        "lastModified": 1765913099,
         "narHash": "sha256-81IuI/Q/y9QG5gLK4ZKzlHC+mVb2SvbyS71Ro2FmOK8=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "86c3e53196ff3c08049e464821bcbebbb9ee8ba6",
+        "rev": "ee3a6aeb480713b2e69618117d0e0ff5562091d1",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
-        "ref": "manifest/v4.26.0",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index caf3581..a947657 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.follows = "lean4-nix/nixpkgs";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix/manifest/v4.26.0";
+    lean4-nix.url = "github:lenianiva/lean4-nix";
   };
 
   outputs = inputs @ {
@@ -26,7 +26,6 @@
         pkgs,
         self',
         config,
-        lib,
         ...
       }: let lake2nix = pkgs.callPackage lean4-nix.lake {};
         in {
@@ -40,7 +39,6 @@
           lake2nix.mkPackage {
             name = "LSpec";
             src = ./.;
-            roots = ["LSpec"];
           };
 
         devShells.default = pkgs.mkShell {