diff --git a/LSpec/SlimCheck/Control/Random.lean b/LSpec/SlimCheck/Control/Random.lean
index 9d3b348..f19a68a 100644
--- a/LSpec/SlimCheck/Control/Random.lean
+++ b/LSpec/SlimCheck/Control/Random.lean
@@ -33,13 +33,13 @@ namespace SlimCheck
 /-- A monad to generate random objects using the generic generator type `g` -/
 abbrev RandT (g : Type) := StateM (ULift g)
 
-instance inhabitedRandT [Inhabited g] [Inhabited α] : Inhabited (RandT g α) where 
+instance inhabitedRandT [Inhabited g] [Inhabited α] : Inhabited (RandT g α) where
   default := fun _ => pure (default, .up default)
 
 /-- A monad to generate random objects using the generator type `Rng` -/
 abbrev Rand (α : Type u) := RandT StdGen α
 
-instance inhabitedStdGen : Inhabited StdGen where 
+instance inhabitedStdGen : Inhabited StdGen where
   default := mkStdGen
 
 /-- `Random α` gives us machinery to generate values of type `α` -/
@@ -76,7 +76,7 @@ namespace Random
 open Rand
 
 /-- Generate a random value of type `α`. -/
-def rand (α : Type u) [Random α] [range : DefaultRange α] [RandomGen g] : RandT g α := 
+def rand (α : Type u) [Random α] [range : DefaultRange α] [RandomGen g] : RandT g α :=
   Random.randomR range.lo range.hi
 
 /-- Generate a random value of type `α` between `x` and `y` inclusive. -/
@@ -84,28 +84,28 @@ def randBound (α : Type u) [Random α] (lo hi : α) [RandomGen g] : RandT g α
   Random.randomR lo hi
 
 def randFin {n : Nat} [RandomGen g] : RandT g (Fin n.succ) :=
-  λ ⟨g⟩ => randNat g 0 n.succ |>.map Fin.ofNat ULift.up
+  λ ⟨g⟩ => randNat g 0 n.succ |>.map (Fin.ofNat' _) ULift.up
 
 instance : Random Bool where
-  randomR := fun lo hi g => 
+  randomR := fun lo hi g =>
     let (n, g') := RandomGen.next g.down
     match lo, hi with
-    | true, false => (n % 2 == 1, .up g') 
+    | true, false => (n % 2 == 1, .up g')
     | false, true => (n % 2 == 0, .up g') -- this doesn't matter btw, I'm just being quirky
     | x, _ => (x, .up g')
 
 instance : Random Nat where
-  randomR := fun lo hi g => 
-    let (n, g') := randNat g.down lo hi 
+  randomR := fun lo hi g =>
+    let (n, g') := randNat g.down lo hi
     (n, .up g')
 
 instance {n : Nat} : Random (Fin n.succ) where
-  randomR := fun lo hi g => 
-    let (n, g') := randNat g.down lo hi  
-    (.ofNat n, .up g')
+  randomR := fun lo hi g =>
+    let (n, g') := randNat g.down lo hi
+    (.ofNat' _ n, .up g')
 
 instance : Random Int where
-  randomR := fun lo hi g => 
+  randomR := fun lo hi g =>
     let lo' := if lo > hi then hi else lo
     let hi' := if lo > hi then lo else hi
     let hi'' := (hi' - lo').toNat
diff --git a/LSpec/SlimCheck/Sampleable.lean b/LSpec/SlimCheck/Sampleable.lean
index f6bdf88..62f3563 100644
--- a/LSpec/SlimCheck/Sampleable.lean
+++ b/LSpec/SlimCheck/Sampleable.lean
@@ -162,7 +162,7 @@ instance Nat.sampleableExt : SampleableExt Nat :=
   mkSelfContained (do choose Nat 0 (← getSize))
 
 instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) :=
-  mkSelfContained (do choose (Fin n.succ) (Fin.ofNat 0) (Fin.ofNat (← getSize)))
+  mkSelfContained (do choose (Fin n.succ) (Fin.ofNat' _ 0) (Fin.ofNat' _ (← getSize)))
 
 instance Int.sampleableExt : SampleableExt Int :=
   mkSelfContained (do choose Int (-(← getSize)) (← getSize))
@@ -221,4 +221,4 @@ instance sampleableExt [SampleableExt α] [Repr α] : SampleableExt (NoShrink α
 
 end NoShrink
 
-end SlimCheck
\ No newline at end of file
+end SlimCheck