Chore: update Lean to v4.26.0

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

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 =>

flake.nix

@@ -27,18 +27,19 @@
         self',
         config,
         ...
-      }: {
+      }: let lake2nix = pkgs.callPackage lean4-nix.lake {};
+        in {
         _module.args.pkgs = import nixpkgs {
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
 
         # 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];

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.26.0