chore: Bump Lean to v4.18.0 (#58)

samuelburnham · web-flow · commit 24cceb69c20f · 2025-04-09T10:01:49.000-04:00
* chore: Bump Lean to v4.18.0

* Prep for merge
diff --git a/LSpec/SlimCheck/Gen.lean b/LSpec/SlimCheck/Gen.lean
@@ -63,15 +63,15 @@ def listOf (x : Gen α) : Gen (List α) :=
 def oneOf [Inhabited α] (xs : Array (Gen α)) : Gen α := do
   let i ← choose Nat 0 (xs.size - 1)
   if h : i < xs.size then
-    xs.get i h
+    xs[i]
   else -- The array is empty
     pure default
 
 /-- Given an array of examples, choose one. -/
 def elements [Inhabited α] (xs : Array α) : Gen α := do
   let i ← choose Nat 0 (xs.size - 1)
   if h : i < xs.size then
-    return xs.get i h
+    return xs[i]
   else -- The array is empty
     pure default
 
diff --git a/flake.lock b/flake.lock
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0
