Merge pull request #9 from leanprover-community/bump_toolchain_to_v4.…

…15.0-rc1

chore: bump toolchain to v4.15.0-rc1

Plausible/Gen.lean

@@ -91,7 +91,7 @@ def listOf (x : Gen α) : Gen (List α) := do
 /-- Given a list of example generators, choose one to create an example. -/
 def oneOf (xs : Array (Gen α)) (pos : 0 < xs.size := by decide) : Gen α := do
   let ⟨x, _, h2⟩ ← up <| chooseNatLt 0 xs.size pos
-  xs.get ⟨x, h2⟩
+  xs[x]
 
 /-- Given a list of examples, choose one to create an example. -/
 def elements (xs : List α) (pos : 0 < xs.length) : Gen α := do

Plausible/Random.lean

@@ -137,7 +137,7 @@ def randBound (α : Type u) [LE α] [BoundedRandom m α] (lo hi : α) (h : lo 
 Generate a random `Fin`.
 -/
 def randFin {n : Nat} [RandomGen g] : RandGT g m (Fin n.succ) :=
-  fun ⟨g⟩ => return randNat g 0 n |>.map Fin.ofNat ULift.up
+  fun ⟨g⟩ => return randNat g 0 n |>.map (Fin.ofNat' _) ULift.up
 
 instance {n : Nat} : Random m (Fin n.succ) where
   random := randFin

Plausible/Sampleable.lean

@@ -157,7 +157,7 @@ instance Nat.shrinkable : Shrinkable Nat where
   shrink := Nat.shrink
 
 instance Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ) where
-  shrink m := Nat.shrink m |>.map Fin.ofNat
+  shrink m := Nat.shrink m |>.map (Fin.ofNat' _)
 
 instance BitVec.shrinkable {n : Nat} : Shrinkable (BitVec n) where
   shrink m := Nat.shrink m.toNat |>.map (BitVec.ofNat n)
@@ -269,7 +269,7 @@ instance Nat.sampleableExt : SampleableExt Nat :=
 instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) :=
   mkSelfContained do
     let m ← choose Nat 0 (min (← getSize) n) (Nat.zero_le _)
-    return Fin.ofNat m
+    return (Fin.ofNat' _ m)
 
 instance BitVec.sampleableExt {n : Nat} : SampleableExt (BitVec n) :=
   mkSelfContained do

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0-rc1",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "plausible",

lakefile.toml

@@ -12,4 +12,4 @@ name = "Plausible"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "v4.14.0"
+rev = "v4.15.0-rc1"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.15.0-rc1