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

View file

@ -46,7 +46,7 @@ Take the integer log base 10 of an `Integer`
View an integer as a list of digits, ordered from least significant digit to
most significant digit.
For a clarifying example:
For a clarifying example:
<!-- idris
-- @@test Ascending Digits Example
@ -62,9 +62,9 @@ For a clarifying example:
```
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 can be reproduced by multiplying the rest by 10 and then adding the
current digit.
a raw integer and by a recursive `Ascending`. Acts as a proof that the number
can be reproduced by multiplying the rest by 10 and then adding the current
digit.
```idris
||| 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
```idris
export
ascList : {i : Integer} -> Ascending i -> List Integer
@ -116,7 +117,7 @@ Convert an `Ascending` to a list
View an integer as a list of digits, ordered from most significant digit to
least significant digit.
For a clarifying example:
For a clarifying example:
<!-- idris
-- @@test Descending Digits Example
@ -132,12 +133,12 @@ For a clarifying example:
```
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 can be reproduced by appending the current digit to the rest of the
number.
a raw integer and by a recursive `Ascending`. Acts as a proof that the number
can be reproduced by appending the current digit to the rest of the number.
```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
data Descending : Integer -> Type where
||| Indicates that the number was negative
@ -180,10 +181,10 @@ Convert a `Descending` to a list
decList : {i : Integer} -> Descending i -> List Integer
decList ds = reverse $ decList' ds []
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' Start acc = acc
decList' (Prev magnitude digit rest rec) acc =
decList' rec (digit :: acc)
```

View file

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