Compare commits

..

2 commits

Author SHA1 Message Date
bfe2b577c1 Add Util.Digits modules
Contains views for seeing integers as lists of digits
2025-01-19 23:59:07 -05:00
cf3a81fa62 Year 2015 Day 9 Part 2 2025-01-19 23:59:07 -05:00
2 changed files with 12 additions and 12 deletions
src
Util
Years/Y2015

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 a raw integer and by a recursive `Ascending`. Acts as a proof that the number
number can be reproduced by multiplying the rest by 10 and then adding the can be reproduced by multiplying the rest by 10 and then adding the current
current digit. 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,6 +98,7 @@ 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
@ -132,12 +133,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 a raw integer and by a recursive `Ascending`. Acts as a proof that the number
number can be reproduced by appending the current digit to the rest of the can be reproduced by appending the current digit to the rest of the number.
number.
```idris ```idris
||| A view of an integer as a list of digits in order of descending signifigance ||| A view of an integer as a list of digits in order of descending
||| 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
@ -180,10 +181,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) -> List Integer decList' : {i : Integer} -> Descending i -> (acc : 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,4 +292,3 @@ public export
day9 : Day day9 : Day
day9 = Both 9 part1 part2 day9 = Both 9 part1 part2
--> -->