Compare commits
2 commits
82268350cb
...
bfe2b577c1
Author | SHA1 | Date | |
---|---|---|---|
bfe2b577c1 | |||
cf3a81fa62 |
2 changed files with 12 additions and 12 deletions
|
@ -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)
|
||||
```
|
||||
|
||||
|
|
|
@ -292,4 +292,3 @@ public export
|
|||
day9 : Day
|
||||
day9 = Both 9 part1 part2
|
||||
-->
|
||||
|
||||
|
|
Loading…
Add table
Reference in a new issue