import Lake open Lake DSL package «aoc-2023» where lean_lib «Day1» where lean_lib «Day2» where lean_lib «Day3» where lean_lib «Day4» where lean_lib «Day5» where lean_lib «Day6» where lean_lib «Day7» where lean_lib «Day8» where lean_lib «Day9» where lean_lib «Day10» where lean_lib «Day11» where lean_lib «Day12» where lean_lib «Day13» where lean_lib «Day14» where lean_lib «Day15» where lean_lib «Day16» where lean_lib «Day17» where lean_lib «Common» where @[default_target] lean_exe «aoc-2023» where root := `Main -- Enables the use of the Lean interpreter by the executable (e.g., -- `runFrontend`) at the expense of increased binary size on Linux. -- Remove this line if you do not need such functionality. supportInterpreter := true require BinaryHeap from git "http://git.grois.info/BinaryHeap"@"ff5c64836ede27d87dbc56b3869021ad8b0d255b" require «lean-astar» from git "http://git.grois.info/lean-astar"@"2539ac49ab6af74b31d91e03d7dbfceedc9c1f02"