Lean/2024/01: Add solution

Author: Defelo

Lean/2024/01.lean

@@ -0,0 +1,32 @@
+def Input := List Int × List Int
+
+def parse (input : String) : Input :=
+  input
+    |>.trim
+    |>.splitOn "\n"
+    |>.map (
+      fun line => line
+        |>.splitOn " "
+        |>.filter (not ∘ String.isEmpty)
+        |>.map String.toInt!
+        |> fun nums => (nums.head!, nums.getLast!)
+      )
+    |>.unzip
+
+def part1 (input : Input) : Nat :=
+  let fst := input.fst.mergeSort (· ≤ ·)
+  let snd := input.snd.mergeSort (· ≤ ·)
+  fst
+    |>.zip snd
+    |>.map (fun (a, b) => a - b |>.natAbs)
+    |>.foldl Nat.add 0
+
+def part2 (input : Input) : Int :=
+  input.fst
+    |>.map (fun a => a * (input.snd.count a))
+    |>.foldl Int.add 0
+
+def main (args : List String) : IO Unit := do
+  let input ← parse <$> (System.FilePath.mk args[0]! |> IO.FS.readFile)
+  IO.println $ part1 input
+  IO.println $ part2 input

Lean/justfile

@@ -0,0 +1,23 @@
+alias r := run
+alias e := example
+alias t := test
+alias ty := test-year
+alias ta := test-all
+
+_default:
+    @just --list
+
+run year day *args:
+    lean --run {{args}} {{year}}/{{day}}.lean ../.cache/{{year}}/{{trim_start_match(day, "0")}}
+
+example year day ex:
+    lean --run {{year}}/{{day}}.lean ../examples/{{year}}/{{trim_start_match(day, "0")}}/{{ex}}
+
+test year day:
+    @diff <(just run {{year}} {{day}}) <(cat ../.cache/{{year}}/{{trim_start_match(day, "0")}}.{1,2})
+
+test-year year:
+    @set -e; for day in $(ls {{year}}); do just test {{year}} $(basename $day .lean); done
+
+test-all:
+    @set -e; for year in *; do [[ -d $year ]] && [[ "$year" =~ ^[0-9]+$ ]] || continue; just test-year $year; done

README.md

@@ -1,5 +1,5 @@
 # AdventOfCode
-[Advent of Code](https://adventofcode.com/) solutions in [<img height=12 src=".assets/rs.svg"> Rust](Rust), [<img height=12 src=".assets/ua.png"> Uiua](Uiua), [<img height=12 src=".assets/py.svg"> Python](Python), [<img height=12 src=".assets/apl.svg"> APL](APL), [<img height=12 src=".assets/hs.svg"> Haskell](Haskell), [<img height=12 src=".assets/rb.svg"> Ruby](Ruby), [<img height=12 src=".assets/nix.svg"> Nix](Nix) and [<img height=12 src=".assets/nu.svg"> Nu](Nu)
+[Advent of Code](https://adventofcode.com/) solutions in [<img height=12 src=".assets/rs.svg"> Rust](Rust), [<img height=12 src=".assets/ua.png"> Uiua](Uiua), [<img height=12 src=".assets/py.svg"> Python](Python), [<img height=12 src=".assets/apl.svg"> APL](APL), [<img height=12 src=".assets/hs.svg"> Haskell](Haskell), [<img height=12 src=".assets/rb.svg"> Ruby](Ruby), [<img height=12 src=".assets/nix.svg"> Nix](Nix), [ Lean](Lean) and [<img height=12 src=".assets/nu.svg"> Nu](Nu)
 
 ### Global Leaderboard Placement
 |Year|Rank|Score|Top% (Leaderboard)|Top% (All participants)|
@@ -9,10 +9,10 @@
 |[2021](https://adventofcode.com/2021/leaderboard)|**136**|438|13.41% (of 1014)|0.0532% (of &ge;255548)|
 |[2020](https://adventofcode.com/2020/leaderboard)|**621**|46|65.23% (of 952)|0.3146% (of &ge;197402)|
 
-## [2024](https://adventofcode.com/2024) ([<img height=18 src=".assets/rs.svg"> Rust](Rust/2024): 25/25 | [<img height=18 src=".assets/ua.png"> Uiua](Uiua/2024): 25/25 | [<img height=18 src=".assets/rb.svg"> Ruby](Ruby/2024): 5/25 | [<img height=18 src=".assets/hs.svg"> Haskell](Haskell/2024): 4/25 | [<img height=18 src=".assets/nix.svg"> Nix](Nix/2024): 1/25)
+## [2024](https://adventofcode.com/2024) ([<img height=18 src=".assets/rs.svg"> Rust](Rust/2024): 25/25 | [<img height=18 src=".assets/ua.png"> Uiua](Uiua/2024): 25/25 | [<img height=18 src=".assets/rb.svg"> Ruby](Ruby/2024): 5/25 | [<img height=18 src=".assets/hs.svg"> Haskell](Haskell/2024): 4/25 | [<img height=18 src=".assets/nix.svg"> Nix](Nix/2024): 1/25 | [ Lean](Lean/2024): 1/25)
 |Mo|Tu|We|Th|Fr|Sa|Su|
 |-|-|-|-|-|-|-|
-|||||||[**1**](https://adventofcode.com/2024/day/1) [<img height=12 src=".assets/rs.svg">](Rust/2024/01.rs "Rust solution for 2024/01") [<img height=12 src=".assets/hs.svg">](Haskell/2024/01.hs "Haskell solution for 2024/01") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgrCsOKKn-KNieKKnOKKnOKLleKIqeKJoEBcbixAIC4K4oipLyviioMo4pmtw5fiip7iirg9fOKMtS3iiKnijYYpCg== "Uiua solution for 2024/01") [<img height=12 src=".assets/nix.svg">](Nix/2024/01.nix "Nix solution for 2024/01") [<img height=12 src=".assets/rb.svg">](Ruby/2024/01.rb "Ruby solution for 2024/01")|
+|||||||[**1**](https://adventofcode.com/2024/day/1) [<img height=12 src=".assets/rs.svg">](Rust/2024/01.rs "Rust solution for 2024/01") [<img height=12 src=".assets/hs.svg">](Haskell/2024/01.hs "Haskell solution for 2024/01") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgrCsOKKn-KNieKKnOKKnOKLleKIqeKJoEBcbixAIC4K4oipLyviioMo4pmtw5fiip7iirg9fOKMtS3iiKnijYYpCg== "Uiua solution for 2024/01") [<img height=12 src=".assets/nix.svg">](Nix/2024/01.nix "Nix solution for 2024/01") [<img height=12 src=".assets/rb.svg">](Ruby/2024/01.rb "Ruby solution for 2024/01") [Lean](Lean/2024/01.lean "Lean solution for 2024/01")|
 |[**2**](https://adventofcode.com/2024/day/2) [<img height=12 src=".assets/rs.svg">](Rust/2024/02.rs "Rust solution for 2024/02") [<img height=12 src=".assets/hs.svg">](Haskell/2024/02.hs "Haskell solution for 2024/02") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipwo4pah4oqc4ouVKeKIqeKJoEBcbixAIC4KCkNoZWNrIOKGkCDDl-KKgygvw5fiiaQz4oy1fOKJjcKkMeKMteKXtMKxKeKniC0K4oipLyviiaHil4fiioMoL-KGpeKJoShDaGVja-KWvSniip7iiaAu4oeh4qe74p-cwqR8Q2hlY2spCg== "Uiua solution for 2024/02") [<img height=12 src=".assets/rb.svg">](Ruby/2024/02.rb "Ruby solution for 2024/02")|[**3**](https://adventofcode.com/2024/day/3) [<img height=12 src=".assets/rs.svg">](Rust/2024/03.rs "Rust solution for 2024/03") [<img height=12 src=".assets/hs.svg">](Haskell/2024/03.hs "Haskell solution for 2024/03") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgrilr3irJoxXCjihqXihqfiipnCsOKKnynijYniip_CrOKIqeKMlSJkb24ndCgpIiwiZG8oKSIuLgriiKkoLysvw5fii5Xihpgx4o2JcmVnZXgibXVsXFwoKFxcZCspLChcXGQrKVxcKSIpCg== "Uiua solution for 2024/03") [<img height=12 src=".assets/rb.svg">](Ruby/2024/03.rb "Ruby solution for 2024/03")|[**4**](https://adventofcode.com/2024/day/4) [<img height=12 src=".assets/rs.svg">](Rust/2024/04.rs "Rust solution for 2024/04") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiJjiiaBAXG4uCgripLAg4oaQIOKIqeKKleKWoeKKmSzijZzima3iipviip7iioMtK-KIqeKHocKw4oqf4oq44pazCgrin5woLyviiaHil4coLyvijJUiWE1BUyIp4oqC4p-c4o2a4oeM4oqC4oqDKOKKguKksHziioLiiKniiaHilqHin5zijYkpKQovK-KZreKniCjDl-KIqSgv4oal4omh4omN4pahIk1BUyLiioLin5zijZrih4wp4qSwKTNfMwo= "Uiua solution for 2024/04") [<img height=12 src=".assets/rb.svg">](Ruby/2024/04.rb "Ruby solution for 2024/04")|[**5**](https://adventofcode.com/2024/day/5) [<img height=12 src=".assets/rs.svg">](Rust/2024/05.rs "Rust solution for 2024/05") [<img height=12 src=".assets/hs.svg">](Haskell/2024/05.hs "Haskell solution for 2024/05") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriioPihpjihpniiqLiiprijJUiXG5cbiIuCuKKmSjiipziipzii5XiiKniiaBAXG4sQHwuKQriipwo4pah4oqc4ouVKeKIqeKJoEBcbixALC4KCk1pbiAgICDihpAg4oqi4pa9wqziirjiiIo64p-cKOKJoeKKo-KWveKIiuKKmeKKuOKJoeKKoikKUmVtb3ZlIOKGkCDiioLiioMo4oaZfOKGmCsxKeKKouKKmuKKuD0KU29ydCAgIOKGkCDiipnii4Xil4zijaIo4oqD4oqC4ouFUmVtb3Zl4oqZ4pehTWlufOKJoDDip7vil4wpW10KTWlkICAgIOKGkCDiio_ijIrDtzLiirjip7sKCuKIqSgvK-KJoeKXh01pZOKWvSkgwqwsLOKKuOKJoeKJjSDin5zijZpTb3J04oqZwqQK "Uiua solution for 2024/05") [<img height=12 src=".assets/rb.svg">](Ruby/2024/05.rb "Ruby solution for 2024/05")|[**6**](https://adventofcode.com/2024/day/6) [<img height=12 src=".assets/rs.svg">](Rust/2024/06.rs "Rust solution for 2024/06") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiJjiiaBAXG4uCgpJbml0ICDihpAgwq8xXzDiiqLiipo9QF4KU3RlcCAg4oaQIOKorCjin5wrfOKHjOKNnOKKosKvKT1AI-KXoSjirJpALuKKoSspClZhbGlkIOKGkCAvw5fDl-KIqT7CrzEu4oqZ4pazCgptYXAuW10g4oq4SW5pdAomcOKKuOKnuyDiipnii4Xil4zijaIo4oqDKGluc2VydOKKmTA64oqZ4peMfOKLhVN0ZXApfOKLheKLhVZhbGlkKQoKU2tpcEZvcndhcmQg4oaQIOKNoijin5wrfMOX4oqDKOKLhVZhbGlkfOKJoEAj4qyaQC7iiqErKSkKQ2hlY2tDeWNsZSDihpAgKAogIG1hcC5bXSDiirhJbml0CiAg4o2iKOKKgyhpbnNlcnTiipkwOuKKmeKKgnzih4zijZziiqLCr1NraXBGb3J3YXJk4peMKXzCrGhhc-KWoTriipniioIpCiAgVmFsaWTii4Xil4wKKQoK4pa9PUAu4peh4oqh4oqZ4peMwrBtYXAKJnAgLyviiaF3YWl04omhcG9vbChDaGVja0N5Y2xl4o2c4oqh4ouFQCMp4oqZwqQK "Uiua solution for 2024/06")|[**7**](https://adventofcode.com/2024/day/7) [<img height=12 src=".assets/rs.svg">](Rust/2024/07.rs "Rust solution for 2024/07") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=IyBFeHBlcmltZW50YWwhCgomc2MKCuKKnCjiipnilqHCsOKKguKKnOKLlSniiaBAXG4swqziirjiiIoiOiAiCgpDaGVjayEg4oaQIHwyIOKNoygKICA94oqZwrDCpAp8IOKNoyjijaQuLkNoZWNrIV4w4o2c4oipKOKHjMKw4ouVKeKMneKKgl4wfOKNpC4uQ2hlY2shXjDijaQuPTDiioPil7_Dt3xDaGVjayFeMC0pIDriipnijZzih4zCsOKKgikKCuKIqSgvK8OXKeKJoSjin5w64p-c4oqDQ2hlY2sh4oiYQ2hlY2shKOKNpC4wKeKKmcKw4pahKQo= "Uiua solution for 2024/07")|[**8**](https://adventofcode.com/2024/day/8) [<img height=12 src=".assets/rs.svg">](Rust/2024/08.rs "Rust solution for 2024/08") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiJjiiaBAXG4uCgpWYWxpZCDihpAgL8OXw5fiiKk-wq8xLgpXYWxrICDihpAg4oqZ4ouF4ouF4peM4o2iKOKKgyjiioLiipnil4x84ouF4p-cKyl84ouF4ouFVmFsaWQp4oavMC7iirgtCgriiaEo4pah4qeFPDLiipo9KeKKmcKk4pa94oq44omgQC7il7Tiirjima3in5wowqTCpOKWsykKCkEg4oaQIOKNmuKJoSjilqHilr064p-c4omhVmFsaWTiip_iiKkoK-KKuC0p4pehOsKw4oqfKQpCIOKGkCDijZriiaEo4pah4oqC4oipV2FsayDil6EoOuKKmeKKmeKImCnCsOKKnykKCuKIqSjip7vil7Qv4peH4oqC4o2aL-KXh-KKgikg4oqDQiBBCg== "Uiua solution for 2024/08")|
 |[**9**](https://adventofcode.com/2024/day/9) [<img height=12 src=".assets/rs.svg">](Rust/2024/09.rs "Rust solution for 2024/09") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=IyBFeHBlcmltZW50YWwhCgomc2MKCuKJoeKLleKWveKKuOKIiitAMOKHoTEwCgp-RmlsZSB7UG9zIExlbiBJZH0KCuKJoShGaWxlwrDiip8pOuKHoeKKuOKnu8Kw4oqf4qS4MeKsmjDihq_iiJ5fMl8y4o2J4oqfOuKfnC3in5xcKwoKU29sdmUg4oaQICgKICDih4ziipko4oqV4pahOsKw4oqf4o2JfDApCiAg4peM4oinKAogICAg4oqZKOKNoyjCsMKkfDAp4pa9KeKfnD3iirgv4oan4omh4peHL-KGp-KKj-KXoeKKmeKLheKImCDijZwt4oeh4oqZ4peh4ouF4qe74oq4RmlsZX5MZW4KICAgIOKorCjil4zil4wKICAgIHwg4oqDKOKNnEZpbGV-UG9z4peMOuKKmeKXjAogICAgICB8IOKNnOKKj-KNnMKw4pah4oqCOuKNmijilr3iirjiiaAp4oqZ4o2c4pah4oKD4oeMOuKKk-KKuCstLOKKmSg6fEZpbGV-TGVuKSkKICAgICnDl-KXoeKKgyg-4oqZ4ouFRmlsZX5Qb3N8PjDil4wpCiAgICDiipkrOi8rw5cr4oqZ4oehwrBGaWxlCiAgKQopCgriiKlTb2x2ZSDin5woLC_il4fiioLijZoo4omhRmlsZeKKmTEr4oehOsKwRmlsZSkpCg== "Uiua solution for 2024/09")|[**10**](https://adventofcode.com/2024/day/10) [<img height=12 src=".assets/rs.svg">](Rust/2024/10.rs "Rust solution for 2024/10") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiaHii5XiirjiiaBAXG4KCk5laWdoIOKGkCDilr09KzHiirjiiqI64p-c4qyaMOKKoSviioIwW-KXoeKIqcKv4p-c4oeM4oehMl3CpAriiKkvK-KJoSjiiKnip7vin5zil7TiiaHil4fiiqNwYXRoKE5laWdofD054oqhKSniipo9MOKfnMKkCg== "Uiua solution for 2024/10")|[**11**](https://adventofcode.com/2024/day/11) [<img height=12 src=".assets/rs.svg">](Rust/2024/11.rs "Rust solution for 2024/11") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipzii5XiirjiiIorQDDih6ExMAoKTmV4dCAg4oaQIOKNoyjCpDHCsDB84omh4ouV4oavMl_iiJ7CsDDil78y4oq44qe7wrDii5V8wqTDlzIwMjQpCkJsaW5rIOKGkCDiiKco4oinKOKNnOKsmjBnZXQr4oqZOilOZXh0KcKwbWFw4oqZKG1hcC5bXSkKCi8r4o2lQmxpbms1MCDin5wvK-KNpUJsaW5rMjUgbWFw4oqV4oqD4oqi4qe74oq44oqbCg== "Uiua solution for 2024/11")|[**12**](https://adventofcode.com/2024/day/12) [<img height=12 src=".assets/rs.svg">](Rust/2024/12.rs "Rust solution for 2024/12") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiJjiirjiiaBAXG4KCuKKnOKWoSsx4oqD4o2c4pmt4oqbKOKHoeKWsykKCkEg4oaQIC8r4omhKC8rwqziiIo6K-KKguKfnMKv4ouvMV8ywqQp4p-cwqQKQiDihpAgKAogIOKXtOKZreKCguKKnistMcOXMuKLr-KHoTTin5zCpMOXMgogIC8r4omhKOKGpeKKgyjil78yLyt8w5cyL8OX4qeI4omgKeKIijorLTHDlzLijZzihpjigoLih4zii6_ih6E0wqQpCikKCuKIqSgvK8OXKeKKmSziiaHil4fiioNCIEEg4p-c4omh4peH4qe7Cg== "Uiua solution for 2024/12")|[**13**](https://adventofcode.com/2024/day/13) [<img height=12 src=".assets/rs.svg">](Rust/2024/13.rs "Rust solution for 2024/13") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgrihq_iiJ5fM18y4oqc4ouV4oq44oiKK0Aw4oehMTAKCivCpFsuMCAxMDAwMDAwMDAwMDAwMF0uCuKIqSgvK-KJoeKNoygvK8OXM18x4omhKMKvwrAw4oqDL-KXvy_Dt-KniCgvLcOX4oeMKSniip_in5zijZzihpnigoLih4x8MCkpCg== "Uiua solution for 2024/13")|[**14**](https://adventofcode.com/2024/day/14) [<img height=12 src=".assets/rs.svg">](Rust/2024/14.rs "Rust solution for 2024/14") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipzii5XiirjiiIriioJALStAMOKHoTEwCuKGmTLiioLiipkxMDFfMTAz4oqD4oaY4oaZwq_ijZwo4pe_NCnii4Uw4oq44qe7CuKGr-KInl8yXzI6CgpTaW0g4oaQIOKXvzorw5fiipkoOsKw4oqf4qS4wq8yfMKkKQoKQSDihpAgL8OX4oqV4qe7LuKKm-KWveKJoDAvw5fiirjijYnCsS0rMcOXMuKKmcKk4oq4U2ltMTAwCkIg4oaQIOKKouKKmj3iirgv4oan4oy1L-KEguKNicO34oqD4qe7LyvCsOKImi3CpMO34oqD4qe7Lysu4qS4MVNpbeKHoS_Dl-KkmeKIqcKkCgriioNCIEEK "Uiua solution for 2024/14")|[**15**](https://adventofcode.com/2024/day/15) [<img height=12 src=".assets/rs.svg">](Rust/2024/15.rs "Rust solution for 2024/15") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgrCsCQiX1xuXG5fIgriipziiJjiirjiiaBAXG4K4oqP4oqX4oqZKCJ2Pl48IuKKguKfnMKv4ouvMV8yKSDilr3iirjiiIoiPD5ediI6CgpOZXh0IOKGkCAoCiAgOuKGr-KKmSgr4peh4ouF4oqZ4ouF4ouF4oiYKeKKuOKIiiJAT1tdIiDiiqHil6Hiipnii4Xii4Xii4XiiJgg4oqZ4oqZ4o2c4oqh4ouFMeKfnDoKICDiioLiqKwo4oqCKzBfMXziioItMF8xfOKXjCniipfiipkoIltdIjopCikKVGFyZ2V0cyDihpAg4oqa4ouF4oqZ4ouF4peM4o2iKOKorChOZXh0fOKXjCniiqHil6Hiipnii4XiiJjCsOKKgnziiaAw4qe7KSDCpOKKmSjiiLXii4UwLCk6Ck1vdmUg4oaQICgKICDCsDAv4oalPUAj4oqh4peh4ouF4oqZ4oiYIOKfnOKKuFRhcmdldHMKICDijZziiqHil4wrwqTiipko4p-c4o2c4oqh4omhKEAu4oiYKSDilr3iiaBALuKXoeKKoSkKKQpTb2x2ZSAg4oaQIC8r4pmtw5fCpDEwMF8x4oqa4oiKIk9bIiDil4ziiKfijaMo4oqDK01vdmV84peMKSDiipko4oqi4oqa4oq4PUBAKQpFeHBhbmQg4oaQIOKNnOKNieKZreKCguKorCgiLi4ifCIjIyJ8IkAuInwiW10iKeKItSjiipfiipkiLiNATyIpCgriiKlTb2x2ZSAsRXhwYW5kLAo= "Uiua solution for 2024/15")|
 |[**16**](https://adventofcode.com/2024/day/16) [<img height=12 src=".assets/rs.svg">](Rust/2024/16.rs "Rust solution for 2024/16") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiJjiirjiiaBAXG4KClN0ZXAg4oaQICgKICBb4o2cwrDiip_iirgrIOKfnOKNnOKKoyjih4zijZziiqPCrykg4p-c4o2c4oqjKOKNnOKKo8Kv4oeMKV0KICDiiKnihpjin5w6PUAj4oqh4oqZ4qSZ4oqZ4oqZ4peM4oqi4oqiLCBbMSAuMTAwMF0KKQoK4oqf4oqZMF8x4oqi4oqa4oq4PUBTCuKnu-KXtOKKouKkuDEv4peH4oqCIHBhdGgoU3RlcHw9QEXiiqHiiqIpCg== "Uiua solution for 2024/16")|[**17**](https://adventofcode.com/2024/day/17) [<img height=12 src=".assets/rs.svg">](Rust/2024/17.rs "Rust solution for 2024/17") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=IyBFeHBlcmltZW50YWwhCgomc2MKCuKKg-KGmeKGmDPiipzii5XiirjiiIorQDDih6ExMAoKQ29tYm8g4oaQIOKKj-KKlzrih6EzLTTiipniioLin5w6CgpBZHYg4oaQIOKNnOKKouKNnOKLr_CdhIjihpg64oq4Q29tYm8KQnhsIOKGkCDijZziio_igoHijZziiKnii6_irJow4omgOgpCc3Qg4oaQIOKNnOKKj-KCgeKXjDril7844oq4Q29tYm8KSm56IOKGkCDiqKwo4peMfOKKmSgtMnzil4wpOiniiaAw4oqiLApCeGMg4oaQIOKNnOKGmOKCgeKNnMKw4oqf4oq44o2c4oip4ouv4qyaMOKJoOKXjApPdXQg4oaQIOKKmeKKmeKKmeKKguKkmuKLheKKmeKKmeKKmeKImOKXvzjiirhDb21ibwpCZHYg4oaQIOKNnOKKj-KCgeKXjDrijZzii6_wnYSI4oaY4oqiLOKKuENvbWJvCkNkdiDihpAg4o2c4oqP4oKC4peMOuKNnOKLr_CdhIjihpjiiqIs4oq4Q29tYm8KClN0ZXAg4oaQIOKKmSvigoLiqKwoQWR2fEJ4bHxCc3R8Sm56fEJ4Y3xPdXR8QmR2fENkdikgwrDiip_iio8r4oehMuKXoeKLheKKmeKImApSdW4gIOKGkCDii4Xii4Xil4zijaIoU3RlcHw-4ouF4oqZ4qe7KeKKmSgwfFtdKQoKQ2hlY2sg4oaQIOKJjeKKmeKGmTogwq_iipko4oq4UnVu4o2c4oqi4peMOikKCuKXoCgv4peHKOKKguKKgilALMKw4ouVUnVuKQov4oan4oqj4oqj4o2JIHBhdGgo4pa9OuKfnOKJoShDaGVja8Kw4oqfKeKKmeKIqcKkK-KNieKKnzDih6E4wqTijZzCsOKKn-KKkyvigoHDl-KCiHw94oqT4oqi4ouF4qe7KTBfMAriiKkmcAo= "Uiua solution for 2024/17")|[**18**](https://adventofcode.com/2024/day/18) [<img height=12 src=".assets/rs.svg">](Rust/2024/18.rs "Rust solution for 2024/18") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipzii5XiirjiiIorQDDih6ExMAriqKwoWy43MV0xMDI0fOKKg-KGmeKCguKKo-KKg-KGmeKGmDMp4pe_MuKKuOKnuwo64oinKOKNnOKKoeKXjOKHjOKKmTopOuKHoeKKuOKnu-KGr-KInl8yOuKKmTrihq_iipniiJ4KClNQIOKGkCDil4xwYXRoKOKKuOKJoeKLhTHilr064p-c4qyaMOKKoeKKguKKgy0r4ouvMV8ywqR84omNKzHiipnilrMpMF8w4omlCgpMQiEg4oaQIOKKo-KNoijijZziiqHil4w64oqZKOKLheKKmeKXjOKXoeKKmV4w4oie4oyKw7cyKeKfnC8rfD4rMcKw4oqfKeKKnwoK4oipJnAgJCJfLF8iwrDiip_ih4ziiqLiipo9LTFMQiEoPeKInlNQKSAwKzEv4oal4pa94oq44omg4oie4oq44pmtIDriirhTUAo= "Uiua solution for 2024/18")|[**19**](https://adventofcode.com/2024/day/19) [<img height=12 src=".assets/rs.svg">](Rust/2024/19.rs "Rust solution for 2024/19") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipzilqHiirjiiaBAXG4gOuKKnOKWocKs4oq44oiKIiwgIsKwJCJfXG5cbl8iCgpEUCDihpAgfDIgbWVtbyjiqKwoLyviiaHil4dEUOKWveKJoeKJjeKKmeKNmuKKg-KsmkBcMOKGmeKGmOKfnOKJoeKXh-Knu-KKmeKIqcKkLHwxKT0w4oq44qe7KQoK4oipLyvin5zihqfigoF3YWl04omh4peHcG9vbERQ4oqZwqQK "Uiua solution for 2024/19")|[**20**](https://adventofcode.com/2024/day/20) [<img height=12 src=".assets/rs.svg">](Rust/2024/20.rs "Rust solution for 2024/20") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipziiJjiirjiiaBAXG4KCsKwwqTiirhwYXRoKOKWveKJoEAjOuKfnOKKoeKKguKKgyst4ouvMV8ywqR8PUBT4oqhKeKKouKKmuKKuD1ARQoKU29sdmUg4oaQICgKICDima3igovigoHiip4o4oqf4p-cKyniirg64pa94oip4pmt4oKL4oKB4omlLyvCsOKNieKMteKfnDriip7iip8u4o2cLeKHoeKKg8KvK-KCgS4KICDiipniipnil4zilr3il6Eo4omgQCPirJpAI-KKoeKKo-KkuDHiipnii4XiiJgpCiAgwrDiip_ipLgxIOKKmSjijZziiqHiiLXil4zin5ziioMowrDiipp84oeh4qe7KSkKICAvK-KJpTEwMC0r4oqDKC8r4o2J4oy1LXziiKniiqHiipksKQopCgriioMoU29sdmUyMHxTb2x2ZTIpCg== "Uiua solution for 2024/20")|[**21**](https://adventofcode.com/2024/day/21) [<img height=12 src=".assets/rs.svg">](Rust/2024/21.rs "Rust solution for 2024/21") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipzilqHiirjiiaBAXG4KClNlcXMg4oaQICgKICDiiaEo4oqi4oqaKT3iipkowqTiipziiJjiirjiiaBAXG4pCiAgwrDCpOKkuDLiip4o4pahcGF0aCjilr3iirjiiIo64oqC4oqDKy3ii68xXzLCpOKKmeKXjHziiY0pKS7in5zCpAogIOKJoeKNmijiiaHiioLiipk04oqX4oqZW8KvMV8wIDBfwq8xIDFfMCAwXzFd4omh4qeILSkKKQoKJCA3ODkKJCA0NTYKJCAxMjMKJCAgMEEKU2VxcyAiMDEyMzQ1Njc4OUEiCk51bVNlcXMg4oaQCgokICBeQQokIDx2PgpTZXFzICJePHY-QSIKRGlyU2VxcyDihpAKCk5leHQhIOKGkCDiiaHigoIoL-KGp-KJoSgvK-KKoeKniOKKn-KKgjQpwrDilqHiiqHiipleMCniipnijaXigoPCpOKHoeKWs14wCgpTb2x2ZSDihpAgKAogIE5leHQhTnVtU2VxcyDijaVOZXh0IURpclNlcXMgLTE6IOKJoeKJoeKXhyjip7viiqIpRGlyU2VxcwogIC8rw5fiiaHil4fiioMoLyviiqHip4jiip_iioIxMOKKl-KKmSIwMTIzNDU2Nzg5QSJ84ouV4pa94oq44oiKK0Aw4oehMTApOsKkCikKCuKKgyhTb2x2ZTI1fFNvbHZlMikK "Uiua solution for 2024/21")|[**22**](https://adventofcode.com/2024/day/22) [<img height=12 src=".assets/rs.svg">](Rust/2024/22.rs "Rust solution for 2024/22") [<img height=12 src=".assets/ua.png">](https://uiua.org/pad?src=JnNjCgriipzii5XiirjiiaBAXG4KCuKHjFvijaXiirgo4o2c4oqZKOKNieKLryniiKfirJowKOKGmTI04omg4p-c4o2cKOKnu-KHjCkrOik2X8KvNV8xMSldMjAwMAoKOi8r4oq44oqjCgrijZzima3igoLiipviiKnCsOKNieKniOKKn-KChOKKg-KniC3ihpjigoTil78xMAov4oal4oqVLyviiKkv4peH4oqC4o2aKOKIqeKWveKfnDriirjil7ApCg== "Uiua solution for 2024/22")|

flake.nix

@@ -159,6 +159,9 @@
           # Ruby
           ruby
           solargraph
+
+          # Lean
+          lean4
         ];
         PYTHONPATH = ".";
         LIBCLANG_PATH = with pkgs; lib.makeLibraryPath [llvmPackages.clang-unwrapped.lib];

scripts/generate-readme.py

@@ -14,6 +14,7 @@
     "nix": "Nix",
     "nu": "Nu",
     "rb": "Ruby",
+    "lean": "Lean",
 }
 exts = {
     "rs": [".rs"],
@@ -24,13 +25,14 @@
     "nix": [".nix"],
     "nu": [".nu"],
     "rb": [".rb"],
+    "lean": [".lean"],
 }
 
 logos = {k.name.split(".")[0]: str(k) for k in Path(".assets").iterdir()}
 
 
 def logo(lang, height=12):
-    return f'<img height={height} src="{logos[lang]}">'
+    return f'<img height={height} src="{logos[lang]}">' if lang in logos else ""
 
 
 def link(year, day, lang):
@@ -51,7 +53,7 @@ def link(year, day, lang):
         else:
             url = f"{names[lang]}/{year}/{day:02}{ext}"
 
-        return f' [{logo(lang)}]({url} "{names[lang]} solution for {year}/{day:02}")'
+        return f' [{logo(lang) or names[lang]}]({url} "{names[lang]} solution for {year}/{day:02}")'
 
     return ""