Compare commits

..

3 commits

Author SHA1 Message Date
82268350cb Add Util.Digits modules
Contains views for seeing integers as lists of digits
2025-01-19 23:54:14 -05:00
bef05278c2 Typo fix 2025-01-19 21:50:20 -05:00
ed3d8a86ca Year 2015 Day 9 Part 2 2025-01-19 18:51:21 -05:00
2 changed files with 12 additions and 12 deletions

View file

@ -62,9 +62,9 @@ For a clarifying example:
``` ```
The view itself, storing the current digit, and the rest of the number, both as The view itself, storing the current digit, and the rest of the number, both as
a raw integer and by a recursive `Ascending`. Acts as a proof that the number a raw integer and by a recursive `Ascending`. Acts as a proof that the
can be reproduced by multiplying the rest by 10 and then adding the current number can be reproduced by multiplying the rest by 10 and then adding the
digit. current digit.
```idris ```idris
||| A view of an integer as a list of digits in order of ascending signifigance ||| A view of an integer as a list of digits in order of ascending signifigance
@ -98,7 +98,6 @@ Generate an `Ascending` from an integer.
``` ```
Convert an `Ascending` to a list Convert an `Ascending` to a list
```idris ```idris
export export
ascList : {i : Integer} -> Ascending i -> List Integer ascList : {i : Integer} -> Ascending i -> List Integer
@ -133,12 +132,12 @@ For a clarifying example:
``` ```
The view itself, storing the current digit, and the rest of the number, both as The view itself, storing the current digit, and the rest of the number, both as
a raw integer and by a recursive `Ascending`. Acts as a proof that the number a raw integer and by a recursive `Ascending`. Acts as a proof that the
can be reproduced by appending the current digit to the rest of the number. number can be reproduced by appending the current digit to the rest of the
number.
```idris ```idris
||| A view of an integer as a list of digits in order of descending ||| A view of an integer as a list of digits in order of descending signifigance
||| signifigance
public export public export
data Descending : Integer -> Type where data Descending : Integer -> Type where
||| Indicates that the number was negative ||| Indicates that the number was negative
@ -181,10 +180,10 @@ Convert a `Descending` to a list
decList : {i : Integer} -> Descending i -> List Integer decList : {i : Integer} -> Descending i -> List Integer
decList ds = reverse $ decList' ds [] decList ds = reverse $ decList' ds []
where where
decList' : {i : Integer} -> Descending i -> (acc : List Integer) -> decList' : {i : Integer} -> Descending i -> (acc : List Integer) -> List Integer
List Integer
decList' (NegDec rec) acc = decList' rec acc decList' (NegDec rec) acc = decList' rec acc
decList' Start acc = acc decList' Start acc = acc
decList' (Prev magnitude digit rest rec) acc = decList' (Prev magnitude digit rest rec) acc =
decList' rec (digit :: acc) decList' rec (digit :: acc)
``` ```

View file

@ -292,3 +292,4 @@ public export
day9 : Day day9 : Day
day9 = Both 9 part1 part2 day9 = Both 9 part1 part2
--> -->