merge

leanprover-community · Dec 2, 2024 · 7d0da3f · 7d0da3f
2 parents d64043d + d1fe662
commit 7d0da3f
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.15.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.15.0-rc1
		leanprover/lean4:v4.15.0-rc1