From 9e0c7a039ee36e5a627cf8f04a8eb910859d97d4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:53:18 +1100
Subject: [PATCH 1/5] bump toolchain/batteries

---
 lake-manifest.json | 2 +-
 lean-toolchain     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index c31b7fc..3ceeba5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "44f2360f50d0d3aea24653103a3f11ef5de9eb90",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 0bef727..9e0b2f2 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:nightly-2024-11-12

From bd638d705be70a9c9c6612625c68bc18f8c74f26 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:53:42 +1100
Subject: [PATCH 2/5] bump toolchain/batteries

---
 lake-manifest.json | 4 ++--
 lakefile.toml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 3ceeba5..5faba09 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "44f2360f50d0d3aea24653103a3f11ef5de9eb90",
+   "rev": "9ba2e12ce6570b7fed7ad4d3675e5f6632949f2b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "plausible",
diff --git a/lakefile.toml b/lakefile.toml
index 982a6a3..a3374ed 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,4 +12,4 @@ name = "Plausible"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "main"
+rev = "nightly-testing"

From 31347da4152838b5d10cc2401eb51dfcf12472d4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:54:09 +1100
Subject: [PATCH 3/5] fixes for ngihtly-2024-11-12

---
 Plausible/Gen.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Plausible/Gen.lean b/Plausible/Gen.lean
index 3d18c1f..9e63748 100644
--- a/Plausible/Gen.lean
+++ b/Plausible/Gen.lean
@@ -92,7 +92,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

From 011b21f0e3f3f25fde64e07130e1a9af4e991742 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 28 Nov 2024 21:52:04 +1100
Subject: [PATCH 4/5] bump toolchain and batteries

---
 lake-manifest.json | 2 +-
 lean-toolchain     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 5faba09..7b2ebdb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9ba2e12ce6570b7fed7ad4d3675e5f6632949f2b",
+   "rev": "030100b990ebf9ba1b15ad90a5bb9607d69e6564",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index 9e0b2f2..b899dce 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-12
+leanprover/lean4:nightly-2024-11-28

From d1fe66272f24fe9bd14bc5b2f3d25a852f26589d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 28 Nov 2024 21:52:38 +1100
Subject: [PATCH 5/5] deprecations

---
 Plausible/Random.lean     | 2 +-
 Plausible/Sampleable.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Plausible/Random.lean b/Plausible/Random.lean
index de4947b..98e1a3e 100644
--- a/Plausible/Random.lean
+++ b/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
diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean
index f12090e..37aeef1 100644
--- a/Plausible/Sampleable.lean
+++ b/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