From 2390fe0a2fbbdd283d21049a1e997026d7d1948c Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Tue, 7 Jan 2025 23:32:53 +0100 Subject: Lean 4.15 --- Day15.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Day15.lean') diff --git a/Day15.lean b/Day15.lean index bb7a01c..5158910 100644 --- a/Day15.lean +++ b/Day15.lean @@ -76,7 +76,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : T let box := updateOrAppend box [] { boxes := old.boxes.set index box - valid := (Array.size_set old.boxes index box).substr old.valid + valid := (Array.size_set old.boxes index box index.isLt).substr old.valid } where updateOrAppend (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) := @@ -95,7 +95,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.remove {α β : T let box := tryRemove box [] { boxes := old.boxes.set index box - valid := (Array.size_set old.boxes index box).substr old.valid + valid := (Array.size_set old.boxes index box index.isLt).substr old.valid } where tryRemove (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) := -- cgit v1.2.3