Add Util.Digits modules

Contains views for seeing integers as lists of digits

src/Util/Digits.md

@@ -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
+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
   ||| 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
-
 ```idris
   export
   ascList : {i : Integer} -> Ascending i -> List Integer
@@ -117,7 +116,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
@@ -133,12 +132,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
+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
-  ||| 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
   data Descending : Integer -> Type where
     ||| Indicates that the number was negative
@@ -181,10 +180,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) -> 
+     decList' : {i : Integer} -> Descending i -> (acc : List Integer) -> 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)
 ```
+

src/Years/Y2015/Day9.md

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