From 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 12 Oct 2025 18:44:32 +0200 Subject: Lean 4.19 --- Day15.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Day15.lean') diff --git a/Day15.lean b/Day15.lean index cf2629d..4490223 100644 --- a/Day15.lean +++ b/Day15.lean @@ -65,8 +65,8 @@ private structure HolidayAsciiStringHelperManualArrangementProcedure (α β : Ty private def HolidayAsciiStringHelperManualArrangementProcedure.empty (α β : Type) : HolidayAsciiStringHelperManualArrangementProcedure α β := { - boxes := Array.mkArray UInt8.size [], - valid := Array.size_mkArray _ _ + boxes := Array.replicate UInt8.size [], + valid := Array.size_replicate } private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (data : β) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β := @@ -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 index.isLt).substr old.valid + valid := (Array.size_set 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 index.isLt).substr old.valid + valid := (Array.size_set index.isLt).substr old.valid } where tryRemove (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) := -- cgit v1.2.3