Merge pull request #20 from leanprover-community/bump_to_v4.19.0-rc1

chore: bump toolchain to v4.19.0-rc1

Author: kim-em

Plausible/Gen.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
 import Plausible.Random
-import Batteries.Data.List.Perm
 
 /-!
 # `Gen` Monad
@@ -106,7 +105,7 @@ def permutationOf : (xs : List α) → Gen { ys // xs ~ ys }
   | x::xs => do
     let ⟨ys, h1⟩ ← permutationOf xs
     let ⟨n, _, h3⟩ ← up <| choose Nat 0 ys.length (by omega)
-    return ⟨insertIdx n x ys, Perm.trans (Perm.cons _ h1) (List.perm_insertIdx _ _ h3).symm⟩
+    return ⟨ys.insertIdx n x, Perm.trans (Perm.cons _ h1) (List.perm_insertIdx _ _ h3).symm⟩
 
 /-- Given two generators produces a tuple consisting out of the result of both -/
 def prodOf {α : Type u} {β : Type v} (x : Gen α) (y : Gen β) : Gen (α × β) := do

Plausible/Sampleable.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
 import Lean.Elab.Command
+import Lean.Meta.Eval
 import Plausible.Gen
 
 /-!
@@ -214,7 +215,7 @@ open Shrinkable
 instance List.shrinkable [Shrinkable α] : Shrinkable (List α) where
   shrink := fun L =>
     (L.mapIdx fun i _ => L.eraseIdx i) ++
-    (L.mapIdx fun i a => (shrink a).map fun a' => L.modify (fun _ => a') i).flatten
+    (L.mapIdx fun i a => (shrink a).map fun a' => L.modify i fun _ => a').flatten
 
 instance ULift.shrinkable [Shrinkable α] : Shrinkable (ULift α) where
   shrink u := (shrink u.down).map ULift.up

lake-manifest.json

@@ -1,15 +1,5 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.18.0-rc1",
-   "inherited": false,
-   "configFile": "lakefile.toml"}],
+ "packages": [],
  "name": "plausible",
  "lakeDir": ".lake"}

lakefile.toml

@@ -8,8 +8,3 @@ name = "Test"
 
 [[lean_lib]]
 name = "Plausible"
-
-[[require]]
-name = "batteries"
-scope = "leanprover-community"
-rev = "v4.18.0-rc1"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.19.0-rc1