My attempts to solve puzzles of Advent of Code
0
fork

Configure Feed

Select the types of activity you want to include in your feed.

From leanpkg to lake

+2083 -5
+2
2021/.gitignore
··· 1 1 /build 2 + /build 3 + /lean_packages
+1 -2
2021/AoC.lean
··· 1 - def main : IO Unit := 2 - IO.println "Hello, world!" 1 + import AoC.Day1
+66
2021/AoC/Day1.lean
··· 1 + namespace Day1 2 + 3 + open IO.FS 4 + 5 + section Common 6 + variable {α β γ ζ : Type u} 7 + variable {a : Type u -> Type v} 8 + 9 + def liftA3 [Applicative a] (f: α -> β -> γ -> ζ) (x: a α) (y: a β) (z: a γ) : a ζ := f <$> x <*> y <*> z 10 + end Common 11 + 12 + section Part1 13 + open Prod 14 + def measureLarge (x: Nat × String) (z: String) : Nat × String := 15 + if x.snd.toNat! < z.toNat! then (x.fst + 1, z) else (x.fst, z) 16 + 17 + def measureLargeNat (x: Nat × Nat) (z: Nat) : Nat × Nat := 18 + if x.snd < z then (x.fst + 1, z) else (x.fst, z) 19 + 20 + def totalIncr (s: Sum Nat String) (xs: Array String := #[]) (ys: Array Nat := #[]): Nat := 21 + match s with 22 + | Sum.inr _ => Prod.fst <| Array.foldl measureLarge (0, Array.get! xs 0) xs 23 + | _ => Prod.fst <| Array.foldl measureLargeNat (0, Array.get! ys 0) ys 24 + 25 + end Part1 26 + 27 + section Part2 28 + 29 + def lookAheadSum? (xs: Array String) (idx: Nat) : OptionM Nat := 30 + let size := xs.size 31 + if size = 0 then 32 + Option.none 33 + else 34 + let x: OptionM Nat := String.toNat! <$> xs.get? idx 35 + let y: OptionM Nat := String.toNat! <$> xs.get? (idx + 1) 36 + let z: OptionM Nat := String.toNat! <$> xs.get? (idx + 2) 37 + liftA3 (· + · + ·) x y z 38 + 39 + 40 + def windowEndIndex (length: Nat): Nat := length - (length % 3) 41 + 42 + /- 43 + below code might look like imperative shit but Lean is smart enough 44 + to convert the same via join points. So, everything gets converted 45 + to functional code in the end 46 + -/ 47 + def threeWindowSums (xs: Array String): Array Nat := do 48 + let mut ys := #[] 49 + for id in [:windowEndIndex xs.size] do 50 + match (lookAheadSum? xs id) with 51 + | some x => ys := ys.push x 52 + | _ => () 53 + return ys 54 + 55 + end Part2 56 + 57 + def run : IO (Nat × Nat) := do 58 + let day1 := "./data/day1.txt" 59 + let readings <- lines day1 60 + 61 + let part1Total := totalIncr (Sum.inr "") readings 62 + let part2Total := totalIncr (Sum.inl 0) (ys := threeWindowSums readings) 63 + 64 + return (part1Total, part2Total) 65 + 66 +
+7
2021/Main.lean
··· 1 + import AoC 2 + 3 + def main : IO Unit := do 4 + let (day1Part1, day1Part2) <- Day1.run 5 + IO.println (day1Part1, day1Part2) 6 + 7 + #eval main
+2000
2021/data/day1.txt
··· 1 + 104 2 + 111 3 + 124 4 + 139 5 + 142 6 + 141 7 + 144 8 + 151 9 + 152 10 + 154 11 + 157 12 + 156 13 + 157 14 + 149 15 + 123 16 + 118 17 + 129 18 + 133 19 + 134 20 + 130 21 + 124 22 + 102 23 + 103 24 + 105 25 + 104 26 + 99 27 + 100 28 + 101 29 + 103 30 + 116 31 + 114 32 + 129 33 + 135 34 + 147 35 + 149 36 + 148 37 + 149 38 + 137 39 + 140 40 + 149 41 + 159 42 + 157 43 + 159 44 + 165 45 + 164 46 + 170 47 + 176 48 + 180 49 + 192 50 + 198 51 + 200 52 + 202 53 + 203 54 + 202 55 + 211 56 + 212 57 + 230 58 + 233 59 + 237 60 + 229 61 + 226 62 + 229 63 + 234 64 + 242 65 + 245 66 + 244 67 + 242 68 + 256 69 + 258 70 + 262 71 + 267 72 + 269 73 + 285 74 + 274 75 + 279 76 + 270 77 + 302 78 + 305 79 + 308 80 + 320 81 + 323 82 + 324 83 + 323 84 + 325 85 + 358 86 + 361 87 + 367 88 + 364 89 + 363 90 + 351 91 + 352 92 + 350 93 + 349 94 + 355 95 + 356 96 + 359 97 + 367 98 + 375 99 + 405 100 + 413 101 + 417 102 + 425 103 + 428 104 + 436 105 + 437 106 + 438 107 + 430 108 + 429 109 + 430 110 + 431 111 + 442 112 + 451 113 + 459 114 + 460 115 + 473 116 + 481 117 + 482 118 + 483 119 + 485 120 + 491 121 + 501 122 + 499 123 + 532 124 + 533 125 + 538 126 + 540 127 + 514 128 + 505 129 + 511 130 + 508 131 + 509 132 + 507 133 + 519 134 + 521 135 + 492 136 + 493 137 + 498 138 + 497 139 + 499 140 + 510 141 + 508 142 + 501 143 + 507 144 + 509 145 + 528 146 + 529 147 + 539 148 + 545 149 + 546 150 + 575 151 + 577 152 + 599 153 + 600 154 + 602 155 + 609 156 + 634 157 + 635 158 + 637 159 + 652 160 + 660 161 + 692 162 + 677 163 + 676 164 + 679 165 + 682 166 + 683 167 + 684 168 + 688 169 + 687 170 + 688 171 + 709 172 + 708 173 + 710 174 + 713 175 + 714 176 + 729 177 + 724 178 + 723 179 + 725 180 + 728 181 + 727 182 + 722 183 + 728 184 + 759 185 + 760 186 + 764 187 + 771 188 + 754 189 + 768 190 + 761 191 + 767 192 + 798 193 + 791 194 + 811 195 + 812 196 + 831 197 + 834 198 + 842 199 + 854 200 + 855 201 + 863 202 + 864 203 + 868 204 + 882 205 + 887 206 + 891 207 + 899 208 + 902 209 + 903 210 + 906 211 + 908 212 + 915 213 + 943 214 + 937 215 + 941 216 + 928 217 + 941 218 + 928 219 + 922 220 + 924 221 + 940 222 + 950 223 + 949 224 + 950 225 + 951 226 + 947 227 + 948 228 + 955 229 + 958 230 + 960 231 + 963 232 + 956 233 + 955 234 + 957 235 + 960 236 + 965 237 + 966 238 + 967 239 + 968 240 + 969 241 + 977 242 + 945 243 + 929 244 + 925 245 + 926 246 + 939 247 + 943 248 + 944 249 + 956 250 + 965 251 + 961 252 + 968 253 + 967 254 + 966 255 + 970 256 + 968 257 + 973 258 + 975 259 + 990 260 + 1003 261 + 1005 262 + 1006 263 + 1009 264 + 1011 265 + 1009 266 + 1015 267 + 1016 268 + 1015 269 + 1000 270 + 1005 271 + 1009 272 + 1005 273 + 1011 274 + 1008 275 + 1017 276 + 1016 277 + 1017 278 + 1018 279 + 1013 280 + 1012 281 + 1015 282 + 1012 283 + 1003 284 + 1004 285 + 1005 286 + 1008 287 + 1016 288 + 1021 289 + 1023 290 + 1051 291 + 1052 292 + 1057 293 + 1059 294 + 1067 295 + 1064 296 + 1060 297 + 1062 298 + 1071 299 + 1065 300 + 1077 301 + 1079 302 + 1081 303 + 1085 304 + 1091 305 + 1089 306 + 1092 307 + 1093 308 + 1103 309 + 1083 310 + 1102 311 + 1111 312 + 1113 313 + 1120 314 + 1131 315 + 1132 316 + 1152 317 + 1153 318 + 1162 319 + 1161 320 + 1160 321 + 1145 322 + 1154 323 + 1159 324 + 1148 325 + 1160 326 + 1161 327 + 1162 328 + 1187 329 + 1193 330 + 1184 331 + 1192 332 + 1190 333 + 1191 334 + 1196 335 + 1200 336 + 1205 337 + 1207 338 + 1209 339 + 1208 340 + 1209 341 + 1210 342 + 1211 343 + 1223 344 + 1225 345 + 1226 346 + 1227 347 + 1217 348 + 1211 349 + 1212 350 + 1216 351 + 1209 352 + 1210 353 + 1219 354 + 1218 355 + 1219 356 + 1220 357 + 1219 358 + 1220 359 + 1215 360 + 1242 361 + 1246 362 + 1247 363 + 1233 364 + 1264 365 + 1297 366 + 1284 367 + 1288 368 + 1313 369 + 1333 370 + 1339 371 + 1334 372 + 1341 373 + 1345 374 + 1351 375 + 1350 376 + 1353 377 + 1349 378 + 1352 379 + 1351 380 + 1352 381 + 1353 382 + 1355 383 + 1333 384 + 1334 385 + 1335 386 + 1336 387 + 1337 388 + 1309 389 + 1316 390 + 1315 391 + 1316 392 + 1325 393 + 1343 394 + 1345 395 + 1347 396 + 1334 397 + 1337 398 + 1336 399 + 1337 400 + 1343 401 + 1346 402 + 1347 403 + 1342 404 + 1328 405 + 1326 406 + 1327 407 + 1328 408 + 1320 409 + 1324 410 + 1334 411 + 1336 412 + 1337 413 + 1338 414 + 1348 415 + 1350 416 + 1358 417 + 1374 418 + 1377 419 + 1380 420 + 1366 421 + 1368 422 + 1372 423 + 1376 424 + 1377 425 + 1380 426 + 1382 427 + 1392 428 + 1396 429 + 1402 430 + 1407 431 + 1408 432 + 1423 433 + 1428 434 + 1422 435 + 1424 436 + 1427 437 + 1440 438 + 1439 439 + 1438 440 + 1454 441 + 1460 442 + 1461 443 + 1462 444 + 1466 445 + 1471 446 + 1470 447 + 1448 448 + 1455 449 + 1460 450 + 1470 451 + 1480 452 + 1488 453 + 1497 454 + 1502 455 + 1503 456 + 1505 457 + 1502 458 + 1503 459 + 1510 460 + 1519 461 + 1523 462 + 1526 463 + 1527 464 + 1526 465 + 1530 466 + 1526 467 + 1536 468 + 1534 469 + 1539 470 + 1553 471 + 1557 472 + 1562 473 + 1569 474 + 1570 475 + 1584 476 + 1601 477 + 1564 478 + 1577 479 + 1582 480 + 1584 481 + 1585 482 + 1586 483 + 1589 484 + 1583 485 + 1595 486 + 1608 487 + 1612 488 + 1610 489 + 1605 490 + 1611 491 + 1615 492 + 1619 493 + 1620 494 + 1621 495 + 1624 496 + 1626 497 + 1628 498 + 1621 499 + 1635 500 + 1637 501 + 1645 502 + 1646 503 + 1656 504 + 1658 505 + 1657 506 + 1667 507 + 1672 508 + 1674 509 + 1675 510 + 1678 511 + 1692 512 + 1693 513 + 1696 514 + 1713 515 + 1714 516 + 1715 517 + 1734 518 + 1736 519 + 1738 520 + 1756 521 + 1757 522 + 1780 523 + 1772 524 + 1777 525 + 1776 526 + 1783 527 + 1786 528 + 1792 529 + 1791 530 + 1792 531 + 1797 532 + 1799 533 + 1794 534 + 1811 535 + 1795 536 + 1793 537 + 1780 538 + 1782 539 + 1791 540 + 1789 541 + 1800 542 + 1799 543 + 1797 544 + 1814 545 + 1812 546 + 1818 547 + 1842 548 + 1853 549 + 1871 550 + 1872 551 + 1876 552 + 1877 553 + 1882 554 + 1883 555 + 1874 556 + 1876 557 + 1879 558 + 1893 559 + 1894 560 + 1911 561 + 1877 562 + 1880 563 + 1883 564 + 1884 565 + 1887 566 + 1885 567 + 1892 568 + 1897 569 + 1912 570 + 1917 571 + 1931 572 + 1934 573 + 1935 574 + 1926 575 + 1930 576 + 1945 577 + 1943 578 + 1942 579 + 1943 580 + 1941 581 + 1943 582 + 1947 583 + 1941 584 + 1950 585 + 1955 586 + 1980 587 + 1981 588 + 1986 589 + 1987 590 + 2000 591 + 2005 592 + 1999 593 + 2009 594 + 2010 595 + 2006 596 + 1998 597 + 1999 598 + 2009 599 + 2016 600 + 2017 601 + 1984 602 + 1985 603 + 1986 604 + 1985 605 + 1988 606 + 2011 607 + 2018 608 + 2019 609 + 2023 610 + 2026 611 + 2034 612 + 2041 613 + 2043 614 + 2060 615 + 2068 616 + 2072 617 + 2079 618 + 2082 619 + 2083 620 + 2077 621 + 2109 622 + 2111 623 + 2118 624 + 2146 625 + 2149 626 + 2151 627 + 2148 628 + 2147 629 + 2137 630 + 2138 631 + 2128 632 + 2138 633 + 2139 634 + 2163 635 + 2164 636 + 2194 637 + 2196 638 + 2197 639 + 2198 640 + 2199 641 + 2201 642 + 2211 643 + 2242 644 + 2244 645 + 2248 646 + 2225 647 + 2226 648 + 2235 649 + 2231 650 + 2232 651 + 2233 652 + 2234 653 + 2237 654 + 2233 655 + 2232 656 + 2235 657 + 2217 658 + 2228 659 + 2234 660 + 2235 661 + 2234 662 + 2237 663 + 2238 664 + 2249 665 + 2250 666 + 2252 667 + 2273 668 + 2261 669 + 2278 670 + 2279 671 + 2275 672 + 2274 673 + 2273 674 + 2271 675 + 2284 676 + 2289 677 + 2282 678 + 2284 679 + 2282 680 + 2283 681 + 2286 682 + 2288 683 + 2302 684 + 2321 685 + 2360 686 + 2368 687 + 2369 688 + 2364 689 + 2373 690 + 2379 691 + 2378 692 + 2386 693 + 2391 694 + 2398 695 + 2399 696 + 2400 697 + 2401 698 + 2409 699 + 2416 700 + 2414 701 + 2413 702 + 2412 703 + 2418 704 + 2406 705 + 2429 706 + 2449 707 + 2446 708 + 2449 709 + 2438 710 + 2448 711 + 2450 712 + 2413 713 + 2422 714 + 2424 715 + 2425 716 + 2429 717 + 2430 718 + 2431 719 + 2426 720 + 2428 721 + 2431 722 + 2417 723 + 2419 724 + 2420 725 + 2427 726 + 2421 727 + 2424 728 + 2433 729 + 2434 730 + 2435 731 + 2436 732 + 2462 733 + 2440 734 + 2443 735 + 2442 736 + 2454 737 + 2455 738 + 2458 739 + 2447 740 + 2448 741 + 2450 742 + 2455 743 + 2462 744 + 2464 745 + 2472 746 + 2477 747 + 2482 748 + 2483 749 + 2501 750 + 2511 751 + 2516 752 + 2517 753 + 2514 754 + 2520 755 + 2521 756 + 2525 757 + 2539 758 + 2553 759 + 2554 760 + 2543 761 + 2548 762 + 2544 763 + 2552 764 + 2551 765 + 2553 766 + 2589 767 + 2588 768 + 2594 769 + 2599 770 + 2614 771 + 2615 772 + 2629 773 + 2630 774 + 2639 775 + 2644 776 + 2646 777 + 2665 778 + 2657 779 + 2668 780 + 2669 781 + 2681 782 + 2680 783 + 2684 784 + 2691 785 + 2693 786 + 2686 787 + 2681 788 + 2680 789 + 2683 790 + 2687 791 + 2694 792 + 2696 793 + 2698 794 + 2702 795 + 2690 796 + 2694 797 + 2693 798 + 2698 799 + 2707 800 + 2716 801 + 2714 802 + 2713 803 + 2714 804 + 2724 805 + 2747 806 + 2748 807 + 2750 808 + 2752 809 + 2760 810 + 2756 811 + 2757 812 + 2755 813 + 2756 814 + 2762 815 + 2765 816 + 2778 817 + 2777 818 + 2778 819 + 2777 820 + 2775 821 + 2778 822 + 2770 823 + 2762 824 + 2754 825 + 2755 826 + 2757 827 + 2770 828 + 2771 829 + 2784 830 + 2815 831 + 2836 832 + 2837 833 + 2838 834 + 2839 835 + 2847 836 + 2848 837 + 2850 838 + 2826 839 + 2806 840 + 2820 841 + 2826 842 + 2827 843 + 2832 844 + 2837 845 + 2848 846 + 2859 847 + 2866 848 + 2865 849 + 2873 850 + 2874 851 + 2876 852 + 2879 853 + 2886 854 + 2861 855 + 2865 856 + 2876 857 + 2875 858 + 2872 859 + 2874 860 + 2879 861 + 2889 862 + 2899 863 + 2908 864 + 2909 865 + 2915 866 + 2903 867 + 2915 868 + 2925 869 + 2918 870 + 2919 871 + 2920 872 + 2936 873 + 2932 874 + 2922 875 + 2923 876 + 2935 877 + 2940 878 + 2947 879 + 2969 880 + 2963 881 + 2940 882 + 2944 883 + 2945 884 + 2949 885 + 2964 886 + 2967 887 + 2968 888 + 2985 889 + 2986 890 + 2973 891 + 2974 892 + 2969 893 + 2970 894 + 2965 895 + 2966 896 + 2967 897 + 2953 898 + 2957 899 + 2956 900 + 2964 901 + 2977 902 + 2974 903 + 2983 904 + 2996 905 + 2994 906 + 2992 907 + 2999 908 + 2988 909 + 2974 910 + 2980 911 + 2985 912 + 2986 913 + 2993 914 + 3007 915 + 3008 916 + 3007 917 + 3014 918 + 3013 919 + 3031 920 + 3027 921 + 3029 922 + 3026 923 + 3027 924 + 3035 925 + 3036 926 + 3037 927 + 3052 928 + 3054 929 + 3055 930 + 3059 931 + 3057 932 + 3059 933 + 3058 934 + 3064 935 + 3063 936 + 3065 937 + 3066 938 + 3070 939 + 3072 940 + 3104 941 + 3111 942 + 3103 943 + 3111 944 + 3112 945 + 3138 946 + 3137 947 + 3150 948 + 3137 949 + 3138 950 + 3139 951 + 3142 952 + 3154 953 + 3156 954 + 3157 955 + 3158 956 + 3160 957 + 3152 958 + 3157 959 + 3143 960 + 3147 961 + 3159 962 + 3161 963 + 3162 964 + 3160 965 + 3163 966 + 3164 967 + 3160 968 + 3161 969 + 3167 970 + 3181 971 + 3182 972 + 3190 973 + 3191 974 + 3193 975 + 3192 976 + 3193 977 + 3205 978 + 3206 979 + 3216 980 + 3229 981 + 3230 982 + 3228 983 + 3230 984 + 3218 985 + 3198 986 + 3205 987 + 3233 988 + 3234 989 + 3222 990 + 3217 991 + 3221 992 + 3242 993 + 3243 994 + 3258 995 + 3275 996 + 3276 997 + 3281 998 + 3283 999 + 3304 1000 + 3303 1001 + 3307 1002 + 3309 1003 + 3308 1004 + 3307 1005 + 3304 1006 + 3315 1007 + 3328 1008 + 3355 1009 + 3375 1010 + 3368 1011 + 3374 1012 + 3403 1013 + 3404 1014 + 3406 1015 + 3409 1016 + 3411 1017 + 3409 1018 + 3392 1019 + 3400 1020 + 3404 1021 + 3405 1022 + 3406 1023 + 3403 1024 + 3405 1025 + 3408 1026 + 3430 1027 + 3439 1028 + 3440 1029 + 3458 1030 + 3461 1031 + 3469 1032 + 3484 1033 + 3490 1034 + 3491 1035 + 3492 1036 + 3506 1037 + 3511 1038 + 3513 1039 + 3524 1040 + 3525 1041 + 3534 1042 + 3535 1043 + 3491 1044 + 3493 1045 + 3509 1046 + 3538 1047 + 3540 1048 + 3545 1049 + 3544 1050 + 3543 1051 + 3552 1052 + 3554 1053 + 3559 1054 + 3565 1055 + 3567 1056 + 3576 1057 + 3580 1058 + 3581 1059 + 3589 1060 + 3594 1061 + 3607 1062 + 3615 1063 + 3618 1064 + 3638 1065 + 3657 1066 + 3665 1067 + 3664 1068 + 3665 1069 + 3658 1070 + 3665 1071 + 3667 1072 + 3668 1073 + 3682 1074 + 3684 1075 + 3687 1076 + 3699 1077 + 3712 1078 + 3716 1079 + 3720 1080 + 3728 1081 + 3744 1082 + 3742 1083 + 3740 1084 + 3752 1085 + 3763 1086 + 3760 1087 + 3757 1088 + 3760 1089 + 3762 1090 + 3767 1091 + 3758 1092 + 3738 1093 + 3739 1094 + 3737 1095 + 3738 1096 + 3762 1097 + 3767 1098 + 3792 1099 + 3820 1100 + 3821 1101 + 3822 1102 + 3824 1103 + 3825 1104 + 3829 1105 + 3821 1106 + 3794 1107 + 3800 1108 + 3799 1109 + 3801 1110 + 3800 1111 + 3820 1112 + 3835 1113 + 3836 1114 + 3856 1115 + 3859 1116 + 3867 1117 + 3871 1118 + 3888 1119 + 3889 1120 + 3893 1121 + 3898 1122 + 3897 1123 + 3894 1124 + 3921 1125 + 3917 1126 + 3916 1127 + 3917 1128 + 3925 1129 + 3922 1130 + 3923 1131 + 3930 1132 + 3931 1133 + 3932 1134 + 3935 1135 + 3936 1136 + 3948 1137 + 3947 1138 + 3948 1139 + 3961 1140 + 3968 1141 + 3998 1142 + 3999 1143 + 4000 1144 + 4001 1145 + 3994 1146 + 3977 1147 + 3979 1148 + 3980 1149 + 3976 1150 + 3982 1151 + 3988 1152 + 3992 1153 + 4000 1154 + 4001 1155 + 4007 1156 + 4008 1157 + 4004 1158 + 4038 1159 + 4025 1160 + 4005 1161 + 3986 1162 + 3987 1163 + 3989 1164 + 3991 1165 + 3983 1166 + 3982 1167 + 4004 1168 + 4005 1169 + 4012 1170 + 4040 1171 + 4060 1172 + 4070 1173 + 4064 1174 + 4086 1175 + 4096 1176 + 4100 1177 + 4109 1178 + 4117 1179 + 4125 1180 + 4142 1181 + 4148 1182 + 4149 1183 + 4154 1184 + 4153 1185 + 4161 1186 + 4162 1187 + 4155 1188 + 4157 1189 + 4159 1190 + 4161 1191 + 4186 1192 + 4202 1193 + 4201 1194 + 4202 1195 + 4201 1196 + 4207 1197 + 4209 1198 + 4212 1199 + 4214 1200 + 4211 1201 + 4212 1202 + 4232 1203 + 4233 1204 + 4239 1205 + 4250 1206 + 4243 1207 + 4242 1208 + 4246 1209 + 4247 1210 + 4246 1211 + 4245 1212 + 4244 1213 + 4251 1214 + 4255 1215 + 4259 1216 + 4261 1217 + 4262 1218 + 4270 1219 + 4252 1220 + 4267 1221 + 4271 1222 + 4272 1223 + 4275 1224 + 4277 1225 + 4276 1226 + 4277 1227 + 4261 1228 + 4275 1229 + 4278 1230 + 4283 1231 + 4304 1232 + 4314 1233 + 4316 1234 + 4323 1235 + 4325 1236 + 4324 1237 + 4331 1238 + 4342 1239 + 4348 1240 + 4352 1241 + 4353 1242 + 4362 1243 + 4389 1244 + 4387 1245 + 4362 1246 + 4360 1247 + 4373 1248 + 4392 1249 + 4393 1250 + 4397 1251 + 4399 1252 + 4400 1253 + 4405 1254 + 4410 1255 + 4405 1256 + 4406 1257 + 4414 1258 + 4403 1259 + 4410 1260 + 4413 1261 + 4417 1262 + 4440 1263 + 4441 1264 + 4442 1265 + 4443 1266 + 4446 1267 + 4459 1268 + 4468 1269 + 4467 1270 + 4475 1271 + 4474 1272 + 4467 1273 + 4473 1274 + 4474 1275 + 4473 1276 + 4472 1277 + 4480 1278 + 4467 1279 + 4468 1280 + 4475 1281 + 4477 1282 + 4478 1283 + 4479 1284 + 4492 1285 + 4493 1286 + 4501 1287 + 4504 1288 + 4503 1289 + 4510 1290 + 4476 1291 + 4482 1292 + 4484 1293 + 4485 1294 + 4486 1295 + 4497 1296 + 4505 1297 + 4512 1298 + 4518 1299 + 4519 1300 + 4521 1301 + 4524 1302 + 4526 1303 + 4533 1304 + 4555 1305 + 4558 1306 + 4573 1307 + 4575 1308 + 4576 1309 + 4564 1310 + 4559 1311 + 4562 1312 + 4573 1313 + 4572 1314 + 4577 1315 + 4580 1316 + 4568 1317 + 4569 1318 + 4570 1319 + 4576 1320 + 4577 1321 + 4578 1322 + 4568 1323 + 4575 1324 + 4582 1325 + 4589 1326 + 4586 1327 + 4599 1328 + 4603 1329 + 4587 1330 + 4618 1331 + 4600 1332 + 4599 1333 + 4598 1334 + 4607 1335 + 4596 1336 + 4608 1337 + 4610 1338 + 4622 1339 + 4626 1340 + 4650 1341 + 4664 1342 + 4679 1343 + 4675 1344 + 4687 1345 + 4685 1346 + 4684 1347 + 4685 1348 + 4680 1349 + 4706 1350 + 4704 1351 + 4693 1352 + 4705 1353 + 4712 1354 + 4713 1355 + 4712 1356 + 4718 1357 + 4728 1358 + 4733 1359 + 4735 1360 + 4759 1361 + 4758 1362 + 4763 1363 + 4764 1364 + 4766 1365 + 4767 1366 + 4793 1367 + 4794 1368 + 4795 1369 + 4796 1370 + 4791 1371 + 4780 1372 + 4761 1373 + 4768 1374 + 4771 1375 + 4777 1376 + 4778 1377 + 4789 1378 + 4788 1379 + 4789 1380 + 4795 1381 + 4802 1382 + 4791 1383 + 4789 1384 + 4790 1385 + 4789 1386 + 4801 1387 + 4809 1388 + 4812 1389 + 4806 1390 + 4826 1391 + 4835 1392 + 4838 1393 + 4840 1394 + 4846 1395 + 4853 1396 + 4856 1397 + 4858 1398 + 4859 1399 + 4864 1400 + 4862 1401 + 4865 1402 + 4867 1403 + 4868 1404 + 4872 1405 + 4875 1406 + 4866 1407 + 4859 1408 + 4860 1409 + 4857 1410 + 4866 1411 + 4872 1412 + 4873 1413 + 4872 1414 + 4884 1415 + 4887 1416 + 4885 1417 + 4895 1418 + 4898 1419 + 4902 1420 + 4901 1421 + 4902 1422 + 4898 1423 + 4887 1424 + 4886 1425 + 4901 1426 + 4913 1427 + 4914 1428 + 4915 1429 + 4918 1430 + 4920 1431 + 4918 1432 + 4959 1433 + 4958 1434 + 4953 1435 + 4982 1436 + 4987 1437 + 4972 1438 + 4988 1439 + 4999 1440 + 4996 1441 + 4997 1442 + 5022 1443 + 5040 1444 + 5038 1445 + 5037 1446 + 5059 1447 + 5062 1448 + 5096 1449 + 5097 1450 + 5102 1451 + 5127 1452 + 5138 1453 + 5176 1454 + 5175 1455 + 5179 1456 + 5180 1457 + 5181 1458 + 5180 1459 + 5213 1460 + 5216 1461 + 5215 1462 + 5214 1463 + 5219 1464 + 5222 1465 + 5225 1466 + 5227 1467 + 5249 1468 + 5286 1469 + 5287 1470 + 5288 1471 + 5302 1472 + 5306 1473 + 5307 1474 + 5316 1475 + 5326 1476 + 5328 1477 + 5327 1478 + 5326 1479 + 5327 1480 + 5305 1481 + 5309 1482 + 5310 1483 + 5305 1484 + 5318 1485 + 5319 1486 + 5322 1487 + 5323 1488 + 5333 1489 + 5355 1490 + 5359 1491 + 5369 1492 + 5368 1493 + 5359 1494 + 5384 1495 + 5387 1496 + 5420 1497 + 5442 1498 + 5453 1499 + 5455 1500 + 5454 1501 + 5446 1502 + 5445 1503 + 5448 1504 + 5455 1505 + 5474 1506 + 5472 1507 + 5478 1508 + 5482 1509 + 5483 1510 + 5490 1511 + 5523 1512 + 5534 1513 + 5535 1514 + 5536 1515 + 5535 1516 + 5537 1517 + 5538 1518 + 5544 1519 + 5547 1520 + 5539 1521 + 5540 1522 + 5558 1523 + 5559 1524 + 5573 1525 + 5574 1526 + 5578 1527 + 5576 1528 + 5584 1529 + 5610 1530 + 5618 1531 + 5609 1532 + 5600 1533 + 5602 1534 + 5627 1535 + 5637 1536 + 5607 1537 + 5603 1538 + 5612 1539 + 5608 1540 + 5611 1541 + 5622 1542 + 5623 1543 + 5625 1544 + 5626 1545 + 5628 1546 + 5634 1547 + 5646 1548 + 5655 1549 + 5658 1550 + 5667 1551 + 5678 1552 + 5682 1553 + 5685 1554 + 5708 1555 + 5712 1556 + 5711 1557 + 5718 1558 + 5716 1559 + 5719 1560 + 5720 1561 + 5722 1562 + 5753 1563 + 5757 1564 + 5752 1565 + 5753 1566 + 5768 1567 + 5774 1568 + 5750 1569 + 5730 1570 + 5728 1571 + 5733 1572 + 5734 1573 + 5729 1574 + 5743 1575 + 5744 1576 + 5746 1577 + 5748 1578 + 5757 1579 + 5771 1580 + 5779 1581 + 5759 1582 + 5763 1583 + 5783 1584 + 5796 1585 + 5797 1586 + 5799 1587 + 5815 1588 + 5816 1589 + 5817 1590 + 5831 1591 + 5838 1592 + 5834 1593 + 5840 1594 + 5846 1595 + 5852 1596 + 5850 1597 + 5858 1598 + 5861 1599 + 5864 1600 + 5867 1601 + 5870 1602 + 5879 1603 + 5903 1604 + 5904 1605 + 5930 1606 + 5931 1607 + 5936 1608 + 5939 1609 + 5941 1610 + 5943 1611 + 5936 1612 + 5938 1613 + 5943 1614 + 5951 1615 + 5962 1616 + 5955 1617 + 5950 1618 + 5945 1619 + 5946 1620 + 5951 1621 + 5950 1622 + 5951 1623 + 5950 1624 + 5956 1625 + 5957 1626 + 5959 1627 + 5975 1628 + 5977 1629 + 5992 1630 + 5994 1631 + 5997 1632 + 5999 1633 + 6011 1634 + 6012 1635 + 6013 1636 + 6014 1637 + 6013 1638 + 6028 1639 + 6032 1640 + 6058 1641 + 6064 1642 + 6065 1643 + 6078 1644 + 6079 1645 + 6080 1646 + 6086 1647 + 6089 1648 + 6091 1649 + 6077 1650 + 6083 1651 + 6051 1652 + 6044 1653 + 6058 1654 + 6062 1655 + 6069 1656 + 6050 1657 + 6048 1658 + 6058 1659 + 6086 1660 + 6093 1661 + 6094 1662 + 6106 1663 + 6107 1664 + 6115 1665 + 6114 1666 + 6115 1667 + 6112 1668 + 6117 1669 + 6131 1670 + 6130 1671 + 6132 1672 + 6140 1673 + 6164 1674 + 6167 1675 + 6163 1676 + 6177 1677 + 6180 1678 + 6181 1679 + 6183 1680 + 6184 1681 + 6186 1682 + 6193 1683 + 6196 1684 + 6197 1685 + 6200 1686 + 6201 1687 + 6198 1688 + 6202 1689 + 6203 1690 + 6193 1691 + 6211 1692 + 6227 1693 + 6222 1694 + 6223 1695 + 6222 1696 + 6224 1697 + 6207 1698 + 6197 1699 + 6198 1700 + 6196 1701 + 6204 1702 + 6206 1703 + 6207 1704 + 6210 1705 + 6209 1706 + 6210 1707 + 6209 1708 + 6229 1709 + 6232 1710 + 6233 1711 + 6235 1712 + 6237 1713 + 6232 1714 + 6254 1715 + 6268 1716 + 6275 1717 + 6290 1718 + 6292 1719 + 6300 1720 + 6301 1721 + 6295 1722 + 6297 1723 + 6298 1724 + 6301 1725 + 6308 1726 + 6317 1727 + 6318 1728 + 6326 1729 + 6319 1730 + 6320 1731 + 6319 1732 + 6321 1733 + 6329 1734 + 6332 1735 + 6331 1736 + 6342 1737 + 6348 1738 + 6369 1739 + 6370 1740 + 6390 1741 + 6420 1742 + 6423 1743 + 6436 1744 + 6437 1745 + 6452 1746 + 6444 1747 + 6445 1748 + 6456 1749 + 6457 1750 + 6444 1751 + 6448 1752 + 6457 1753 + 6489 1754 + 6491 1755 + 6502 1756 + 6507 1757 + 6510 1758 + 6495 1759 + 6497 1760 + 6505 1761 + 6507 1762 + 6511 1763 + 6513 1764 + 6516 1765 + 6520 1766 + 6523 1767 + 6532 1768 + 6534 1769 + 6535 1770 + 6548 1771 + 6561 1772 + 6560 1773 + 6566 1774 + 6567 1775 + 6586 1776 + 6589 1777 + 6592 1778 + 6598 1779 + 6602 1780 + 6603 1781 + 6621 1782 + 6630 1783 + 6632 1784 + 6634 1785 + 6660 1786 + 6661 1787 + 6662 1788 + 6642 1789 + 6657 1790 + 6659 1791 + 6655 1792 + 6658 1793 + 6661 1794 + 6662 1795 + 6663 1796 + 6672 1797 + 6661 1798 + 6664 1799 + 6665 1800 + 6678 1801 + 6682 1802 + 6683 1803 + 6669 1804 + 6663 1805 + 6658 1806 + 6663 1807 + 6680 1808 + 6685 1809 + 6686 1810 + 6687 1811 + 6693 1812 + 6687 1813 + 6680 1814 + 6686 1815 + 6694 1816 + 6676 1817 + 6675 1818 + 6695 1819 + 6698 1820 + 6716 1821 + 6717 1822 + 6720 1823 + 6728 1824 + 6734 1825 + 6735 1826 + 6733 1827 + 6743 1828 + 6745 1829 + 6758 1830 + 6757 1831 + 6763 1832 + 6762 1833 + 6761 1834 + 6790 1835 + 6793 1836 + 6798 1837 + 6799 1838 + 6807 1839 + 6808 1840 + 6822 1841 + 6828 1842 + 6795 1843 + 6793 1844 + 6795 1845 + 6790 1846 + 6791 1847 + 6794 1848 + 6799 1849 + 6808 1850 + 6815 1851 + 6827 1852 + 6856 1853 + 6857 1854 + 6882 1855 + 6883 1856 + 6885 1857 + 6886 1858 + 6903 1859 + 6902 1860 + 6903 1861 + 6904 1862 + 6892 1863 + 6893 1864 + 6912 1865 + 6893 1866 + 6888 1867 + 6887 1868 + 6891 1869 + 6892 1870 + 6891 1871 + 6898 1872 + 6899 1873 + 6900 1874 + 6901 1875 + 6900 1876 + 6901 1877 + 6913 1878 + 6914 1879 + 6918 1880 + 6932 1881 + 6944 1882 + 6945 1883 + 6960 1884 + 6963 1885 + 6961 1886 + 6966 1887 + 6968 1888 + 6974 1889 + 6979 1890 + 6980 1891 + 6981 1892 + 6982 1893 + 7003 1894 + 7023 1895 + 7034 1896 + 7035 1897 + 7068 1898 + 7087 1899 + 7088 1900 + 7089 1901 + 7098 1902 + 7104 1903 + 7093 1904 + 7095 1905 + 7102 1906 + 7129 1907 + 7120 1908 + 7123 1909 + 7153 1910 + 7155 1911 + 7157 1912 + 7158 1913 + 7157 1914 + 7151 1915 + 7167 1916 + 7190 1917 + 7208 1918 + 7197 1919 + 7200 1920 + 7201 1921 + 7224 1922 + 7223 1923 + 7217 1924 + 7224 1925 + 7225 1926 + 7227 1927 + 7228 1928 + 7233 1929 + 7234 1930 + 7265 1931 + 7266 1932 + 7267 1933 + 7286 1934 + 7296 1935 + 7297 1936 + 7299 1937 + 7295 1938 + 7296 1939 + 7297 1940 + 7283 1941 + 7259 1942 + 7255 1943 + 7259 1944 + 7260 1945 + 7267 1946 + 7275 1947 + 7273 1948 + 7274 1949 + 7277 1950 + 7276 1951 + 7289 1952 + 7291 1953 + 7297 1954 + 7298 1955 + 7299 1956 + 7298 1957 + 7300 1958 + 7307 1959 + 7308 1960 + 7312 1961 + 7332 1962 + 7341 1963 + 7342 1964 + 7335 1965 + 7348 1966 + 7349 1967 + 7345 1968 + 7344 1969 + 7345 1970 + 7358 1971 + 7357 1972 + 7359 1973 + 7397 1974 + 7398 1975 + 7401 1976 + 7406 1977 + 7425 1978 + 7424 1979 + 7429 1980 + 7430 1981 + 7433 1982 + 7435 1983 + 7436 1984 + 7437 1985 + 7430 1986 + 7429 1987 + 7439 1988 + 7440 1989 + 7454 1990 + 7456 1991 + 7438 1992 + 7439 1993 + 7421 1994 + 7439 1995 + 7438 1996 + 7441 1997 + 7421 1998 + 7422 1999 + 7424 2000 + 7440
+6
2021/lakefile.lean
··· 1 + import Lake 2 + open Lake DSL 3 + 4 + package AoC { 5 + -- add configuration options here 6 + }
+1
2021/lean-toolchain
··· 1 + leanprover/lean4:nightly-2021-12-04
-3
2021/leanpkg.toml
··· 1 - [package] 2 - name = "AoC" 3 - version = "0.1"