Skip to content

Commit 99d9d4b

Browse files
authored
fix: Subarray->Slice migration (#1292)
1 parent 9072d15 commit 99d9d4b

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

Batteries/Data/Array/Basic.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -163,9 +163,9 @@ def popHead? (as : Subarray α) : Option (α × Subarray α) :=
163163
then
164164
let head := as.array[as.start]'(Nat.lt_of_lt_of_le h as.stop_le_array_size)
165165
let tail :=
166-
{ as with
167-
start := as.start + 1
168-
start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h }
166+
{ as.internalRepresentation with
167+
start := as.start + 1
168+
start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h }
169169
some (head, tail)
170170
else
171171
none

0 commit comments

Comments
 (0)