Skip to content

Commit c8a36c5

Browse files
committed
Fix instance name
1 parent 3690c48 commit c8a36c5

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

‎RandomDo/Monad/ForInInstances.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ instance : MeasurableSpace (Array α) :=
2929
instance {n : ℕ} : MeasurableSpace (Vector α n) :=
3030
MeasurableSpace.comap Vector.toArray inferInstance
3131

32-
instance : MeasurableSpace (Subarray α) :=
32+
instance instMeasurableSpaceSubarray : MeasurableSpace (Subarray α) :=
3333
MeasurableSpace.comap (fun s : Subarray α ↦ s.toList) inferInstance
3434

3535
@[fun_prop]

0 commit comments

Comments
 (0)