diff --git a/README.md b/README.md
index f40d0a7..5bfba46 100644
--- a/README.md
+++ b/README.md
@@ -1,30 +1,24 @@
-# Advent
+# Advent 
 
-The goal of this project is to get all 500 currently available stars in the form
-of one single idris application, and thoroughly document the results as literate
-idris files.
+The goal of this project is to get all 500 currently available stars in the form of one single idris application, and thoroughly document the results as literate idris files.
 
 # Index of non-day modules
 
 - [Runner](src/Runner.md)
 
-  Provides data structures for structuring the division of the project into
-  years, days, and parts.
+  Provides data structures for structuring the division of the project into years, days, and parts.
 
 - [Main](src/Main.md)
 
-Provides the `Runner` based command line interface for running a selected day's
-solution.
+Provides the `Runner` based command line interface for running a selected day's solution.
 
 - [Util](src/Util.md)
 
-  Provides extensions of the functionality of the standard library and external
-  libraries. Extensions to the standard library are in the base of this module.
-
+  Provides extensions of the functionality of the standard library and external libraries. Extensions to the standard library are in the base of this module.
+  
   - [Util.Eff](src/Util/Eff.md)
-
-    Extend the functionality of the effects included in the
-    [eff](https://github.com/stefan-hoeck/idris2-eff/) library
+  
+    Extend the functionality of the effects included in the [eff](https://github.com/stefan-hoeck/idris2-eff/) library
 
 # Index of years and days
 
@@ -36,4 +30,3 @@ solution.
   - [Day 5](src/Years/Y2015/Day5.md)
   - [Day 6](src/Years/Y2015/Day6.md)
   - [Day 7](src/Years/Y2015/Day7.md)
-  - [Day 8](src/Years/Y2015/Day8.md)
diff --git a/src/Grid.md b/src/Grid.md
index ceb6a22..77fa988 100644
--- a/src/Grid.md
+++ b/src/Grid.md
@@ -2,9 +2,7 @@
 
 Types and utilities for dealing with a 2D grid of things
 
-We base our `Grid` type on `Data.Seq.Sized` from `contrib`, a finger tree based
-collection that tracks its size in its type, since it provides somewhat
-efficient random access and updates.
+We base our `Grid` type on `Data.Seq.Sized` from `contrib`, a finger tree based collection that tracks its size in its type, since it provides somewhat efficient random access and updates.
 
 ```idris
 module Grid
@@ -25,8 +23,7 @@ import Decidable.Equality
 
 A coordinate is a pair of numbers both less than their respective bounds.
 
-Since `Grid`s will always be non-empty in the contexts we will be using them in,
-this type alias adds one to each of the bounds to ensure non-emptyness
+Since `Grid`s will always be non-empty in the contexts we will be using them in, this type alias adds one to each of the bounds to ensure non-emptyness
 
 ```idris
 public export
@@ -38,20 +35,11 @@ Coord rows cols = (Fin (S rows), Fin (S cols))
 
 Lazily generate all the coordinates for a given pair of bounds
 
-Uses an internal helper function to generate a lazy list of all the fins of a
-given bound in ascending order (`all`), and another to convert a lazy list of
-`Fin` into a lazy list of pairs of `Fin`s.
+Uses an internal helper function to generate a lazy list of all the fins of a given bound in ascending order (`all`), and another to convert a lazy list of `Fin` into a lazy list of pairs of `Fin`s.
 
-The totality checker likes to go in the descending direction, since then it can
-reason about values getting structurally "smaller", so it has issues with `all'`
-moving in the ascending direction. We know this function is total because the
-`acc < last` check will always eventually be triggered, since `Fin`s only have a
-finite number of values.
+The totality checker likes to go in the descending direction, since then it can reason about values getting structurally "smaller", so it has issues with `all'` moving in the ascending direction. We know this function is total because the `acc < last` check will always eventually be triggered, since `Fin`s only have a finite number of values. 
 
-We pull out an `assert_smaller` to tell Idris that the argument to the recursive
-call is getting structurally smaller, which while not strictly correct, does
-convey to the compiler that we are getting closer to our recursive base case and
-that the function is thus total.
+We pull out an `assert_smaller` to tell Idris that the argument to the recursive call is getting structurally smaller, which while not strictly correct, does convey to the compiler that we are getting closer to our recursive base case and that the function is thus total.
 
 ```idris
 export
@@ -70,12 +58,9 @@ allCords = concat . map row $ all
     row r = map (\c => (r, c)) all
 ```
 
-Add a given vector to a coordinate, returning `Nothing` if we go off the ends of
-the bounds in the process.
+Add a given vector to a coordinate, returning `Nothing` if we go off the ends of the bounds in the process.
 
-To keep this function simple and reasonably efficient, we perform the arithmetic
-in integer space, using `integerToFin` to fallably convert back to `Fin` space,
-making use of the `Maybe` monad to keep the code clean.
+To keep this function simple and reasonably efficient, we perform the arithmetic in integer space, using `integerToFin` to fallably convert back to `Fin` space, making use of the `Maybe` monad to keep the code clean.
 
 ```idris
 export
@@ -104,8 +89,7 @@ record Grid (rows, cols : Nat) (e : Type) where
 
 ### Constructors
 
-Construct a `Grid` by filling every slot with identical copies of the provided
-element
+Construct a `Grid` by filling every slot with identical copies of the provided element
 
 ```idris
 export
@@ -116,9 +100,7 @@ replicate seed =
   in MkGrid grid
 ```
 
-Attempt to construct a `Grid` from a Foldable of Foldables. Will return
-`Nothing` if either the rows are of heterogeneous size, or if either the rows or
-columns are empty. Requires that the outer Foldable also be Traversable.
+Attempt to construct a `Grid` from a Foldable of Foldables. Will return `Nothing` if either the rows are of heterogeneous size, or if either the rows or columns are empty. Requires that the outer Foldable also be Traversable.
 
 We make heavy use of the `Maybe` monad to keep the code clean here.
 
@@ -151,9 +133,7 @@ fromFoldable xs = do
         No _ => Nothing
 ```
 
-Construct a `Grid` from a non-empty `Vect` of non-empty `Vect`s. To keep the
-function simple, we require that both the row and column dimension are known to
-be non-zero before calling this constructor.
+Construct a `Grid` from a non-empty `Vect` of non-empty `Vect`s. To keep the function simple, we require that both the row and column dimension are known to be non-zero before calling this constructor.
 
 ```idris
 export
@@ -161,7 +141,7 @@ fromVect : Vect (S rows) (Vect (S cols) e) -> Grid rows cols e
 fromVect xs = MkGrid . fromVect . map fromVect $ xs
 ```
 
-Construct `Grid` containing the coordinate of the location in each location
+Construct `Grid` containing the coordinate of the location in each location 
 
 ```idris
 export
@@ -316,8 +296,7 @@ Extensions of the above functionality
 
 #### Indexing
 
-Convert this grid to one with both the index of the location and the element in
-each location
+Convert this grid to one with both the index of the location and the element in each location
 
 ```idris
 export
@@ -326,7 +305,6 @@ indexed grid = zip coordinateGrid grid
 ```
 
 Same as `flat` above, but indexed
-
 ```idris
 export
 flatIndexed : {rows, cols : Nat} -> Grid rows cols e -> LazyList (Coord rows cols, e)
@@ -335,8 +313,7 @@ flatIndexed = flat . indexed
 
 #### String functionality
 
-Attempts to convert a string, with newline delimited rows, to a grid of
-characters
+Attempts to convert a string, with newline delimited rows, to a grid of characters
 
 ```idris
 export
@@ -363,7 +340,6 @@ toVects (MkGrid grid) = toVect . map toVect $ grid
 ```
 
 Convert a grid to a list of lists
-
 ```idris
 export
 toLists : Grid rows cols e -> List (List e)
diff --git a/src/Main.md b/src/Main.md
index a913135..b859238 100644
--- a/src/Main.md
+++ b/src/Main.md
@@ -1,11 +1,25 @@
+**Table of Contents**
+
+- [Advent of Code](#advent-of-code)
+- [Command Line Interface](#command-line-interface)
+    - [Error Type](#error-type)
+    - [Extract the year and day](#extract-the-year-and-day)
+- [The Advent ](#the-advent)
+- [The Hard Part](#the-hard-part)
+    - [Parsing the arguments](#parsing-the-arguments)
+    - [Handling the arguments and finding the input](#handling-the-arguments-and-finding-the-input)
+    - [Executing the parts](#executing-the-parts)
+    - [Helper functions](#helper-functions)
+        - [Print strings to stderr](#print-strings-to-stderr)
+        - [Decompose a Writer](#decompose-a-writer)
+        - [Lower logging into the IO component of the effect](#lower-logging-into-the-io-component-of-the-effect)
+- [Handle the effectful action as an IO action ](#handle-the-effectful-action-as-an-io-action)
+
 # Advent of Code
 
-This module provides a command line interface for running the solution to a
-specific day for a specific year, run as `advent $YEAR $DAY`.
+This module provides a command line interface for running the solution to a specific day for a specific year, run as `advent $YEAR $DAY`. 
 
-This runner will automatically locate the appropriate input file and then run
-the selected day's solution against it. See [Runner](Runner.md) for the
-definitions of the `Day`, `Year`, and `Advent` data types.
+This runner will automatically locate the appropriate input file and then run the selected day's solution against it. See [Runner](Runner.md) for the definitions of the `Day`, `Year`, and `Advent` data types.
 
 ```idris
 module Main
@@ -35,9 +49,7 @@ import Years.Y2015;
 
 # Command Line Interface
 
-Since this is a simple application, I am using `GetOpt` from `contrib` for
-argument parsing. Here we define our options list, a data type to describe our
-flags, and the usage message header.
+Since this is a simple application, I am using `GetOpt` from `contrib` for argument parsing. Here we define our options list, a data type to describe our flags, and the usage message header.
 
 ```idris
 data Flag = UseExample | Verbose
@@ -56,9 +68,7 @@ header = "Usage: advent YEAR DAY [OPTION...]"
 
 ## Error Type
 
-We will be using one unified error type for the entire `Main` module, but we
-must go ahead and define it before we go any further with command line arguments
-parsing, as we are about to do some things that might fail.
+We will be using one unified error type for the entire `Main` module, but we must go ahead and define it before we go any further with command line arguments parsing, as we are about to do some things that might fail.
 
 ```idris
 data Error : Type where
@@ -73,8 +83,8 @@ data Error : Type where
 %name Error err
 ```
 
-A `Show` implementation for `Error` is provided, hidden in this document for
-brevity.
+A `Show` implementation for `Error` is provided, hidden in this document for brevity.
+
 
 <!-- idris
 Show Error where
@@ -102,11 +112,7 @@ Show Error where
 
 ## Extract the year and day
 
-After peeling off our options from the arguments using `GetOpt`, we will be left
-with a list of non-option arguments, which we must then parse into our year
-number/day number pair. We perform some pattern matching to make sure the list
-is the correct length, and then parse the individual integers, throwing an error
-if anything goes wrong
+After peeling off our options from the arguments using `GetOpt`, we will be left with a list of non-option arguments, which we must then parse into our year number/day number pair. We perform some pattern matching to make sure the list is the correct length, and then parse the individual integers, throwing an error if anything goes wrong
 
 ```idris
 ||| Convert the non-option arguments into a Year/Day pair
@@ -121,12 +127,9 @@ argumentsToPair [year, day] = do
 argumentsToPair xs = throw $ ArgumentsError (length xs)
 ```
 
-# The Advent
+# The Advent 
 
-Construct our top-level `Advent` record from the imported `Year` modules. The
-argument to the `MkAdvent` constructor is a `FreshList`, with a freshness
-criteria ensuring that the list is in ascending order and does not include any
-duplicate `Year`s.
+Construct our top-level `Advent` record from the imported `Year` modules. The argument to the `MkAdvent` constructor is a `FreshList`, with a freshness criteria ensuring that the list is in ascending order and does not include any duplicate `Year`s.
 
 ```idris
 advent : Advent
@@ -137,17 +140,11 @@ advent = MkAdvent [
 
 # The Hard Part
 
-Now we must glue everything together, parse our arguments, handle any supplied
-options, locate the relevant year and day, locate the corresponding input file,
-read it, and then run the selected `Day` against it.
+Now we must glue everything together, parse our arguments, handle any supplied options, locate the relevant year and day, locate the corresponding input file, read it, and then run the selected `Day` against it.
 
-Because we are building our application around effects, the actual core of the
-application is the effectful `start` computation, that the `main` function will
-then apply `IO` based handlers to.
+Because we are building our application around effects, the actual core of the application is the effectful `start` computation, that the `main` function will then apply `IO` based handlers to.
 
-Our reader and writer aren't ready yet, we need to do some setup first, so the
-top level type signature doesn't include them, so we'll add them to the effects
-list as they become available.
+Our reader and writer aren't ready yet, we need to do some setup first, so the top level type signature doesn't include them, so we'll add them to the effects list as they become available.
 
 ```idris
 covering
@@ -158,9 +155,7 @@ start = do
 
 ## Parsing the arguments
 
-Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the
-name the binary was invoked with, then check for any errors in the result,
-throwing our own error if any are encountered.
+Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the name the binary was invoked with, then check for any errors in the result, throwing our own error if any are encountered.
 
 ```idris
   -- Read and parse arguments/options
@@ -170,9 +165,7 @@ throwing our own error if any are encountered.
     throw (OptionsError opts.errors)
 ```
 
-Use our `argumentsToPair` function to extract the selected year and day numbers
-from the positional arguments, implicitly throwing an error if there are any
-failures doing so.
+Use our `argumentsToPair` function to extract the selected year and day numbers from the positional arguments, implicitly throwing an error if there are any failures doing so.
 
 ```idris
   (year, day_n) <- argumentsToPair opts.nonOptions
@@ -180,9 +173,7 @@ failures doing so.
 
 ## Handling the arguments and finding the input
 
-Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise
-blackhole the logs. Afterwards, use `logHandler` to introduce the logging
-`Writer` into the effects list.
+Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise blackhole the logs. Afterwards, use `logHandler` to introduce the logging `Writer` into the effects list.
 
 ```idris
   -- If the verbose flag is set, hook up the logging writer to stderr
@@ -193,13 +184,9 @@ blackhole the logs. Afterwards, use `logHandler` to introduce the logging
   logHandler $ do
 ```
 
-Find the current directory and append to it to find the input file. If the
-`--use-example/-u` flag is set, look for the input file at
-`inputs/examples/$year/$day`, otherwise look for it at `inputs/real/$year/$day`.
+Find the current directory and append to it to find the input file. If the `--use-example/-u` flag is set, look for the input file at `inputs/examples/$year/$day`, otherwise look for it at `inputs/real/$year/$day`.
 
-After we've located it, attempt to read from it, throwing an `InputRead` error
-if any errors occur, then insert the contents into our `Reader` and inject it
-into the effects list.
+After we've located it, attempt to read from it, throwing an `InputRead` error if any errors occur, then insert the contents into our `Reader` and inject it into the effects list.
 
 ```idris
   -- Locate and read in the input file
@@ -214,8 +201,7 @@ into the effects list.
   runReaderAt "input" contents {fs = PartEff Error} $ do
 ```
 
-Try and locate the `Day` in our `Advent` record, throwing an error if we are
-unable to locate it
+Try and locate the `Day` in our `Advent` record, throwing an error if we are unable to locate it
 
 ```idris
   -- Attempt to locate the provided day
@@ -224,9 +210,7 @@ unable to locate it
 
 ## Executing the parts
 
-Run the selected `Day`'s part 1, wrapping any errors that it returns in a
-`SolveError`. Collect both the result and the opaque context value, then print
-out the result.
+Run the selected `Day`'s part 1, wrapping any errors that it returns in a `SolveError`. Collect both the result and the opaque context value, then print out the result.
 
 ```idris
   -- Run part 1
@@ -236,9 +220,7 @@ out the result.
   putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut1} $ part_1
 ```
 
-Check and see if the selected `Day` has a part 2, if it does, feed the opaque
-context value collected from part 1 into it, wrap any errors that it returns in
-a `SolveError`, then print out the result, then return, closing out the program.
+Check and see if the selected `Day` has a part 2, if it does, feed the opaque context value collected from part 1 into it, wrap any errors that it returns in a `SolveError`, then print out the result, then return, closing out the program.
 
 ```idris
   -- Run part 2 if we have it
@@ -259,8 +241,7 @@ a `SolveError`, then print out the result, then return, closing out the program.
 
 ### Lower logging into the IO component of the effect
 
-This function uses the provided `String -> IO ()` to remove the `Writer` from
-the effects list by translating `tell` calls to IO actions within the effect.
+This function uses the provided `String -> IO ()` to remove the `Writer` from the effects list by translating `tell` calls to IO actions within the effect. 
 
 ```idris
     -- Lowers logging into IO within the effect using the given IO function
@@ -274,14 +255,11 @@ the effects list by translating `tell` calls to IO actions within the effect.
              f $ ignore msg) x
 ```
 
-# Handle the effectful action as an IO action
+# Handle the effectful action as an IO action 
 
-Use `runEff` to translate the effects in `start`'s effects list into IO actions,
-and return the resulting `IO ()`.
+Use `runEff` to translate the effects in `start`'s effects list into IO actions, and return the resulting `IO ()`.
 
-The `IO` component of the effects list is handled via `id`, translating `IO`
-actions into themselves, and we construct a helper function to handle errors as
-IO actions by printing the error and crashing the program.
+The `IO` component of the effects list is handled via `id`, translating `IO` actions into themselves, and we construct a helper function to handle errors as IO actions by printing the error and crashing the program.
 
 ```idris
 covering
diff --git a/src/Runner.md b/src/Runner.md
index 500821b..54a09da 100644
--- a/src/Runner.md
+++ b/src/Runner.md
@@ -1,12 +1,23 @@
+**Table of Contents**
+
+- [Unified interface for any day from any year](#unified-interface-for-any-day-from-any-year)
+- [Effectful Parts](#effectful-parts)
+- [The `Day` Record](#the-day-record)
+    - [Smarter Constructors](#smarter-constructors)
+        - [First](#first)
+        - [Both](#both)
+    - [Freshness](#freshness)
+- [The `Year` Record](#the-year-record)
+    - [Freshness](#freshness-1)
+- [The `Advent` Record](#the-advent-record)
+    - [Methods](#methods)
+        - [locate](#locate)
+
 # Unified interface for any day from any year
 
-This module provides some basic data types for building an application
-containing all my solutions to all of the parts of all the days across all of
-the years.
+This module provides some basic data types for building an application containing all my solutions to all of the parts of all the days across all of the years.
 
-This provides a defensively built API for constructing the overall `Advent` data
-structure that prevents registering a day/year twice or registering days/years
-out of order.
+This provides a defensively built API for constructing the overall `Advent` data structure that prevents registering a day/year twice or registering days/years out of order. 
 
 ```idris
 module Runner
@@ -21,18 +32,9 @@ import public Util.Eff
 
 # Effectful Parts
 
-The solution to each part of a day is run as an effectful computation, and as
-the available effects are meant to be the same across both parts, only varying
-in the type of the error value in the `Except` effect, I construct a type level
-function to have a single source of truth for this. The `err` type can be any
-type with a `Show` implementation, but that constraint will be tacked on in the
-next step.
+The solution to each part of a day is run as an effectful computation, and as the available effects are meant to be the same across both parts, only varying in the type of the error value in the `Except` effect, I construct a type level function to have a single source of truth for this. The `err` type can be any type with a `Show` implementation, but that constraint will be tacked on in the next step.
 
-A `Writer` effect is provided for logging, and a `Reader` effect is provided to
-pass in the input, just to make the top level API a little bit cleaner. `IO` is
-also provided, even though the part solutions themselves shouldn't really be
-doing any IO, this may come in handy if a part needs `IO` for performance
-reasons.
+A `Writer` effect is provided for logging, and a `Reader` effect is provided to pass in the input, just to make the top level API a little bit cleaner. `IO` is also provided, even though the part solutions themselves shouldn't really be doing any IO, this may come in handy if a part needs `IO` for performance reasons.
 
 ```idris
 ||| The effect type is the same in boths parts one and two, modulo potentially
@@ -45,20 +47,11 @@ PartEff err =
 
 # The `Day` Record
 
-The `Day` type groups together an effectful `part1` computation, an optional
-effectful `part2` computation, the day number, and does some type wrangling to
-get the type system out of our way on this one.
+The `Day` type groups together an effectful `part1` computation, an optional effectful `part2` computation, the day number, and does some type wrangling to get the type system out of our way on this one.
 
-`part1` and `part2` are allowed independent output and error types, and this
-record captures `Show` implementations for those output and error types so that
-we can display them in `Main` where the `Day` is consumed without having to
-actually know what the types are.
+`part1` and `part2` are allowed independent output and error types, and this record captures `Show` implementations for those output and error types so that we can display them in `Main` where the `Day` is consumed without having to actually know what the types are.
 
-It is often useful to pass a bit of context, such as the data structures
-resulting from parsing, between `part1` and `part2`, and this is achieved by the
-erased `ctx` type, which is totally opaque here. The runner code in `Main` will
-provide the value of the `ctx` type produced as part of the output of `part1` as
-the input of `part2`.
+It is often useful to pass a bit of context, such as the data structures resulting from parsing, between `part1` and `part2`, and this is achieved by the erased `ctx` type, which is totally opaque here. The runner code in `Main` will provide the value of the `ctx` type produced as part of the output of `part1` as the input of `part2`.
 
 ```idris
 ||| Model solving a single day
@@ -78,11 +71,7 @@ record Day where
 
 ## Smarter Constructors
 
-The default `MkDay` constructor is slightly cumbersome to use, always requiring
-_something_ for the `part2` slot, even if there isn't a part 2 yet, and
-requiring that `part2` be wrapped in a `Just` when there is one, so we provide a
-pair of constructors for the case where there is only a `part1` and for where
-there is a `part1` and a `part2` that handle that for us.
+The default `MkDay` constructor is slightly cumbersome to use, always requiring _something_ for the `part2` slot, even if there isn't a part 2 yet, and requiring that `part2` be wrapped in a `Just` when there is one, so we provide a pair of constructors for the case where there is only a `part1` and for where there is a `part1` and a `part2` that handle that for us.
 
 ```idris
 namespace Day
@@ -90,9 +79,7 @@ namespace Day
 
 ### First
 
-The `First` constructor only accepts a `part1`, it does the work of filling in
-`part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for
-us.'
+The `First` constructor only accepts a `part1`, it does the work of filling in `part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for us.'
 
 ```idris
   ||| Constructor for a day with only part one ready to run
@@ -106,8 +93,7 @@ us.'
 
 ### Both
 
-The `Both` constructor does a little bit less heavy lifting, the only thing it
-needs to do for us is wrap `part2` in a `Just`.
+The `Both` constructor does a little bit less heavy lifting, the only thing it needs to do for us is wrap `part2` in a `Just`.
 
 ```idris
   ||| Constructor for a day with both parts ready to run
@@ -122,17 +108,9 @@ needs to do for us is wrap `part2` in a `Just`.
 
 ## Freshness
 
-We will be using a _Fresh List_ from the
-[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build
-defensiveness into the API. A Fresh List structurally only allows you to prepend
-an element onto it when it satisfies some _freshness_ criteria relative to the
-elements already in the list.
+We will be using a _Fresh List_ from the [structures](https://git.sr.ht/~thatonelutenist/Structures) package to build defensiveness into the API. A Fresh List structurally only allows you to prepend an element onto it when it satisfies some _freshness_ criteria relative to the elements already in the list.
 
-Here, we compare the day numbers of the two `Day`s using the less-than
-relationship. Since we are operating on the start of the list when this
-comparison takes place, this enforces, through type checking, that the resulting
-Fresh List is sorted in ascending order and that no two `Day`s have the same day
-number.
+Here, we compare the day numbers of the two `Day`s using the less-than relationship. Since we are operating on the start of the list when this comparison takes place, this enforces, through type checking, that the resulting Fresh List is sorted in ascending order and that no two `Day`s have the same day number.
 
 ```idris
 ||| Freshness criteria for days
@@ -149,8 +127,7 @@ FreshDay x y = x.day < y.day
 
 # The `Year` Record
 
-The `Year` record collects a number of `Day`s into a single Fresh List for the
-year, and is mostly just a simple container.
+The `Year` record collects a number of `Day`s into a single Fresh List for the year, and is mostly just a simple container.
 
 ```idris
 ||| Collect all the days in a given year
@@ -164,11 +141,7 @@ record Year where
 
 ## Freshness
 
-Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored
-in a `FreshList` in `Advent`, so we need to provide a freshness criteria for
-`Year` as well. We do so by applying the less-than relationship against the year
-number of the two `Years`, for the same reasons and with the same results as
-with `FreshDay`.
+Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored in a `FreshList` in `Advent`, so we need to provide a freshness criteria for `Year` as well. We do so by applying the less-than relationship against the year number of the two `Years`, for the same reasons and with the same results as with `FreshDay`.
 
 ```idris
 ||| Freshness criteria for years
@@ -185,9 +158,7 @@ FreshYear x y = x.year < y.year
 
 # The `Advent` Record
 
-The `Advent` record collects a number of `Year`s in much the same way that
-`Year` collects a number of days, sorting the `Year`s in a `FreshList` to
-provide API defensiveness.
+The `Advent` record collects a number of `Year`s in much the same way that `Year` collects a number of days, sorting the `Year`s in a `FreshList` to provide API defensiveness.
 
 ```idris
 ||| Collect all years
@@ -206,12 +177,9 @@ namespace Advent
 
 ### locate
 
-This is a utility function that searches the `FreshList` of `Year`s for the
-provided year number, then searches the resulting `Year`, if one exists, for the
-provided day number.
+This is a utility function that searches the `FreshList` of `Year`s for the provided year number, then searches the resulting `Year`, if one exists, for the provided day number.
 
-We don't have to worry about potentially encountering duplicates here because of
-the freshness restriction.
+We don't have to worry about potentially encountering duplicates here because of the freshness restriction. 
 
 ```idris
   ||| Attempt to locate `Day` entry corresponding to the provided day and year numbers
diff --git a/src/Util.md b/src/Util.md
index 92b301a..1523f8f 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -1,7 +1,6 @@
 # Utility functions
 
-This module contains functions that extend the functionality of standard data
-types, other types of utility functionality get their own module
+This module contains functions that extend the functionality of standard data types, other types of utility functionality get their own module
 
 ```idris
 module Util
@@ -21,8 +20,7 @@ namespace Either
 
 ### mapLeft
 
-Applies a function to the contents of a `Left` if the value of the given
-`Either` is actually a `Left`, otherwise, leaves `Right`s untouched.
+Applies a function to the contents of a `Left` if the value of the given `Either` is actually a `Left`, otherwise, leaves `Right`s untouched.
 
 ```idris
   export
@@ -30,7 +28,6 @@ Applies a function to the contents of a `Left` if the value of the given
   mapLeft f (Left x) = Left (f x)
   mapLeft f (Right x) = Right x
 ```
-
 ## Vectors
 
 Define some operations for pairs of numbers, treating them roughly like vectors
@@ -84,9 +81,7 @@ namespace String
 
 Returns `True` if `needle` is a substring of `haystack`
 
-We first check to see if the needle is a prefix of the top level haystack,
-before calling into a tail recursive helper function that peels one character
-off of the string at a time, checking if the needle is a prefix at each step.
+We first check to see if the needle is a prefix of the top level haystack, before calling into a tail recursive helper function that peels one character off of the string at a time, checking if the needle is a prefix at each step.
 
 ```idris
   export
diff --git a/src/Util/Eff.md b/src/Util/Eff.md
index 40517ea..3d8c95d 100644
--- a/src/Util/Eff.md
+++ b/src/Util/Eff.md
@@ -18,8 +18,7 @@ import System.File
 
 ### Log Levels
 
-Basic enumeration describing log levels, we define some (hidden) utility
-functions for working with these.
+Basic enumeration describing log levels, we define some (hidden) utility functions for working with these.
 
 ```idris
 public export
@@ -80,9 +79,7 @@ levelToTag (Other k) =
 
 ### Logger effect
 
-This is a basic data structure that captures a lazy log message (so we don't
-have to pay any of the costs associated with generating the log message when it
-is filtered)
+This is a basic data structure that captures a lazy log message (so we don't have to pay any of the costs associated with generating the log message when it is filtered)
 
 ```idris
 public export
@@ -90,8 +87,7 @@ data Logger : Type -> Type where
   Log : (level : Level) -> (msg : Lazy String) -> Logger ()
 ```
 
-We'll also provide some basic accessors, and an `ignore` function useful for
-writing handlers.
+We'll also provide some basic accessors, and an `ignore` function useful for writing handlers.
 
 ```idris
 export  
@@ -109,13 +105,9 @@ ignore (Log level msg) = ()
 
 #### Handler
 
-Because we know that we will only be using `logger` in an `IO` context, we
-aren't currently going to provide a `runLogger` or the like, instead we'll
-define a function, suitable for use as a `runEff` handler, that filters log
-messages and prints them to `stderr` over `IO`.
+Because we know that we will only be using `logger` in an `IO` context, we aren't currently going to provide a `runLogger` or the like, instead we'll define a function, suitable for use as a `runEff` handler, that filters log messages and prints them to `stderr` over `IO`.
 
-In the event a log message is filtered out, it's inner message is never
-inspected, avoiding evaluation.
+In the event a log message is filtered out, it's inner message is never inspected, avoiding evaluation.
 
 ```idris
 export
@@ -129,10 +121,7 @@ handleLoggerIO max_level x =
     else pure . ignore $ x
 ```
 
-Use the `WriterL "log" String` effect like a logging library. We'll provide a
-few "log levels" as verbs for the effect, but no filtering is done, when logging
-is enabled, all logs are always displayed, however the log level is indicated
-with a colored tag.
+Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag. 
 
 ```idris
 export
@@ -155,28 +144,3 @@ export
 trace : Has Logger fs => Lazy String -> Eff fs ()
 trace x = send $ Log Trace x
 ```
-
-## Choose
-
-Lifts any foldable data structure into the Choose effect, enabling the style of
-nondeterministic programming from the list monad
-
-```idris
-export
-oneOf : Has (Choose) fs => Foldable f =>
-    f a -> Eff fs a
-oneOf x = foldl oneOf' empty x
-  where
-  oneOf' : Eff fs a -> a -> Eff fs a
-  oneOf' acc val = pure val `alt` acc
-```
-
-Lifts any foldable of effectful computations into the Choose effect much the
-same as `oneOf`
-
-```idris
-export
-oneOfM : Has (Choose) fs => Foldable f =>
-    f (Eff fs a) -> Eff fs a
-oneOfM x = foldl alt empty x
-```
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index d3be367..19be161 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -5,7 +5,6 @@ import Structures.Dependent.FreshList
 
 import Runner
 ```
-
 <!-- idris
 import Years.Y2015.Day1
 import Years.Y2015.Day2
@@ -14,7 +13,6 @@ import Years.Y2015.Day4
 import Years.Y2015.Day5
 import Years.Y2015.Day6
 import Years.Y2015.Day7
-import Years.Y2015.Day8
 -->
 
 # Days
@@ -67,12 +65,7 @@ y2015 = MkYear 2015 [
   , day7
 ```
 
-## [Day 8](Y2015/Day8.md)
-
-```idris
-  , day8
-```
-
 ```idris
   ]
 ```
+
diff --git a/src/Years/Y2015/Day1.md b/src/Years/Y2015/Day1.md
index cfc4950..38c9e42 100644
--- a/src/Years/Y2015/Day1.md
+++ b/src/Years/Y2015/Day1.md
@@ -1,7 +1,6 @@
 # Year 2015 Day 1
 
-Pretty simple, basic warmup problem, nothing really novel is on display here
-except the effectful part computations.
+Pretty simple, basic warmup problem, nothing really novel is on display here except the effectful part computations.
 
 <!-- idris
 module Years.Y2015.Day1
@@ -15,11 +14,9 @@ import Runner
 
 ## Solver Functions
 
-This one implements the entirety of the logic for part 1, in a simple tail
-recursive manner, pattern matching on each character in the input string.
+This one implements the entirety of the logic for part 1, in a simple tail recursive manner, pattern matching on each character in the input string.
 
-We include a case for a non-paren character for totality's sake, but since we
-kinda trust the input here we just don't do anything in that branch.
+We include a case for a non-paren character for totality's sake, but since we kinda trust the input here we just don't do anything in that branch.
 
 ```idris
 trackFloor : (start : Integer) -> (xs : List Char) -> Integer
@@ -29,9 +26,7 @@ trackFloor start (')' :: xs) = trackFloor (start - 1) xs
 trackFloor start (x :: xs) = trackFloor start xs
 ```
 
-This one is slightly more complicated, ultimately very similar to the above, but
-with two accumulators, one for the position in the input string in addition to
-the one for the current floor.
+This one is slightly more complicated, ultimately very similar to the above, but with two accumulators, one for the position in the input string in addition to the one for the current floor.
 
 ```idris
 findBasement : (position : Nat) -> (currentFloor : Integer) -> (xs : List Char)
@@ -53,8 +48,7 @@ Both this parts are simple application of one of our solver functions
 
 ### Part 1
 
-Very uneventful, the only thing novel here is pulling the input out of the
-`ReaderL "input" String`, which will become very boring very quickly.
+Very uneventful, the only thing novel here is pulling the input out of the `ReaderL "input" String`, which will become very boring very quickly.
 
 ```idris
 part1 : Eff (PartEff String) (Integer, ())
@@ -66,8 +60,7 @@ part1 = do
 
 ### Part 2
 
-We have to be careful to start the position accumulator at 1, since the problem
-specifies that the input string is 1-index.
+We have to be careful to start the position accumulator at 1, since the problem specifies that the input string is 1-index.
 
 ```idris
 part2 : () -> Eff (PartEff String) Nat
diff --git a/src/Years/Y2015/Day2.md b/src/Years/Y2015/Day2.md
index 43ca0b1..51641d4 100644
--- a/src/Years/Y2015/Day2.md
+++ b/src/Years/Y2015/Day2.md
@@ -32,9 +32,7 @@ record Box where
 
 ### Box methods
 
-`.area` provides the surface area of the box, `.slack` provides the surface area
-of the smallest face, `.ribbon` provides the smallest perimeter of a face, and
-`.bow` provides the volume of the box.
+`.area` provides the surface area of the box, `.slack` provides the surface area of the smallest face, `.ribbon` provides the smallest perimeter of a face, and `.bow` provides the volume of the box.
 
 Names are as described in the problem
 
@@ -55,16 +53,14 @@ Names are as described in the problem
 (.bow) (MkBox length width height) = length * width * height
 ```
 
-Provide the total amount of ribbon needed, by adding the ribbon (smallest
-perimeter) and the bow (volume) values together.
+Provide the total amount of ribbon needed, by adding the ribbon (smallest perimeter) and the bow (volume) values together.
 
 ```idris
 totalRibbon : Box -> Integer
 totalRibbon x = x.ribbon + x.bow
 ```
 
-Provide the total amount of paper needed by adding the surface area and the
-slack (smallest side surface area) together.
+Provide the total amount of paper needed by adding the surface area and the slack (smallest side surface area) together.
 
 ```idris
 paperNeeded : Box -> Integer
@@ -81,17 +77,14 @@ parseBox : Has (Except String) fs =>
 parseBox str = do
 ```
 
-First, we split the string into 3 parts by pattern matching on the result of
-`split`, using `pure` to lift the computation into the effect, and throwing an
-error if the pattern match fails.
+First, we split the string into 3 parts by pattern matching on the result of `split`, using `pure` to lift the computation into the effect, and throwing an error if the pattern match fails.
 
 ```idris
   l ::: [w, h] <- pure $ split (== 'x') str
     | xs => throw "Box did not have exactly 3 components: \{show xs}"
 ```
 
-Then try to parse each of the three integers, throwing an error if parsing
-fails, then construct and return our box.
+Then try to parse each of the three integers, throwing an error if parsing fails, then construct and return our box.
 
 ```idris
   length <- note "Failed parsing length: \{show l}" $ parsePositive l
@@ -104,11 +97,9 @@ fails, then construct and return our box.
 
 ### Part 1
 
-Split the input into lines, effectfully traverse our box parser over the
-resulting list of lines, then sum the amounts of paper needed for each box.
+Split the input into lines, effectfully traverse our box parser over the resulting list of lines, then sum the amounts of paper needed for each box.
 
-We return the list of parsed boxes as the context here to avoid needing to parse
-again in part 2
+We return the list of parsed boxes as the context here to avoid needing to parse again in part 2
 
 ```idris
 part1 : Eff (PartEff String) (Integer, List Box)
@@ -121,9 +112,7 @@ part1 = do
 
 ### Part 2
 
-Much the same as part 1, except with the amount of ribbon needed instead of the
-amount of paper, and without the parsing, since we received the already parsed
-list of boxes from part 1 as our context value.
+Much the same as part 1, except with the amount of ribbon needed instead of the amount of paper, and without the parsing, since we received the already parsed list of boxes from part 1 as our context value.
 
 ```idris
 part2 : (boxes : List Box) -> Eff (PartEff String) Integer
diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md
index 9dd7ecc..af7f5e2 100644
--- a/src/Years/Y2015/Day3.md
+++ b/src/Years/Y2015/Day3.md
@@ -1,7 +1,6 @@
 # Year 2015 Day 3
 
-This day provides a gentle introduction to `mutual` blocks and mutually
-recursive functions.
+This day provides a gentle introduction to `mutual` blocks and mutually recursive functions. 
 
 <!-- idris
 module Years.Y2015.Day3
@@ -24,16 +23,13 @@ import Util
 
 ## Parsing and data structures
 
-We'll do parsing a little more properly this time, turning the input into a list
-of movement commands
+We'll do parsing a little more properly this time, turning the input into a list of movement commands
 
 ```idris
 data Movement = North | East | South | West
 ```
 
-We need an effectful operation to parse a single char into a movement. We'll
-pattern match on the char, and include a catch-all case that throws an error in
-the event of an invalid char
+We need an effectful operation to parse a single char into a movement. We'll pattern match on the char, and include a catch-all case that throws an error in the event of an invalid char
 
 ```idris
 parseMovement : Has (Except String) fs => (x : Char) -> Eff fs Movement
@@ -44,9 +40,7 @@ parseMovement '<' = pure West
 parseMovement x = throw "Invalid Movement: \{show x}"
 ```
 
-We also need to be able to translate a `Movement` into a vector of length one
-pointing in the given direction in coordinate space. Somewhat arbitrarily, we
-chose 'North' to be positive x and 'East' to be positive y.
+We also need to be able to translate a `Movement` into a vector of length one pointing in the given direction in coordinate space. Somewhat arbitrarily, we chose 'North' to be positive x and 'East' to be positive y.
 
 ```idris
 vector : Movement -> (Integer, Integer)
@@ -60,17 +54,11 @@ vector West = (0, -1)
 
 ### Visited houses
 
-This is a pretty simple task, we are just applying the movements to our current
-position, and adding our current position to the set of visited locations, so
-we'll handle this with a normal tail recursive function.
+This is a pretty simple task, we are just applying the movements to our current position, and adding our current position to the set of visited locations, so we'll handle this with a normal tail recursive function.
 
-To keep the api nice, we wont ask for the set or the starting location in the
-top-level function, and instead have the top level function initialize the set
-and location before passing control to the inner tail-recursive variant.
+To keep the api nice, we wont ask for the set or the starting location in the top-level function, and instead have the top level function initialize the set and location before passing control to the inner tail-recursive variant.
 
-Because the starting location gets a present, we'll add our location to the set
-before performing the movement, so we will need to add our final location to the
-set in the recursive base case.
+Because the starting location gets a present, we'll add our location to the set before performing the movement, so we will need to add our final location to the set in the recursive base case.
 
 ```idris
 visitedLocations : List Movement -> SortedSet (Integer, Integer)
@@ -85,26 +73,13 @@ visitedLocations xs = visitor xs empty (0, 0)
 
 ### Robo Santa
 
-This one gets a bit more interesting, we'll adopt the same tail recursive
-approach, but instead use a `mutual` block and two mutually recursive functions
-to handle the alternation between santa and robo santa. The `visitSanta`
-function will pass control to `visitRobo` after executing its movement, and vise
-versa.
+This one gets a bit more interesting, we'll adopt the same tail recursive approach, but instead use a `mutual` block and two mutually recursive functions to handle the alternation between santa and robo santa. The `visitSanta` function will pass control to `visitRobo` after executing its movement, and vise versa.
 
-We'll want to insert both present deliverer's locations in the recursive base
-case, this may result in a duplicate location, but that's okay because
-`SortedSet` will only hold at most one of each item inserted into it.
+We'll want to insert both present deliverer's locations in the recursive base case, this may result in a duplicate location, but that's okay because `SortedSet` will only hold at most one of each item inserted into it.
 
-In idris, there is a general requirement that values be defined before their
-use, a common feature of dependently typed languages, resulting from the fact
-that just having the type signature of a function/value alone is not always
-enough to perform type checking, as functions can appear as part of types,
-requiring evaluation of the function and making automatic dependency analysis
-effectively impossible.
+In idris, there is a general requirement that values be defined before their use, a common feature of dependently typed languages, resulting from the fact that just having the type signature of a function/value alone is not always enough to perform type checking, as functions can appear as part of types, requiring evaluation of the function and making automatic dependency analysis effectively impossible.
 
-Inside a `mutual` block, elaboration behaves differently, elaborating types
-first and then values in separate passes. This restricts what you can do a
-little, but enables mutually recursive functions.
+Inside a `mutual` block, elaboration behaves differently, elaborating types first and then values in separate passes. This restricts what you can do a little, but enables mutually recursive functions.
 
 ```idris
 visitedLocations' : List Movement -> SortedSet (Integer, Integer)
@@ -128,9 +103,7 @@ visitedLocations' xs = visitSanta xs empty (0, 0) (0, 0)
 
 ### Part 1
 
-Similar to the previous day, we get our input, unpack it, and traverse our
-effectful movement parsing function over it, before feeding that into our
-solving function.
+Similar to the previous day, we get our input, unpack it, and traverse our effectful movement parsing function over it, before feeding that into our solving function.
 
 ```idris
 part1 : Eff (PartEff String) (Nat, List Movement)
diff --git a/src/Years/Y2015/Day4.md b/src/Years/Y2015/Day4.md
index a1fee57..04d5f40 100644
--- a/src/Years/Y2015/Day4.md
+++ b/src/Years/Y2015/Day4.md
@@ -1,7 +1,6 @@
 # Year 2015 Day 4
 
-This day introduces us to a little bit of FFI, linking to openssl to use it's
-`MD5` functionality.
+This day introduces us to a little bit of FFI, linking to openssl to use it's `MD5` functionality.
 
 <!-- idris
 module Years.Y2015.Day4
@@ -20,22 +19,15 @@ import Prim.Array
 
 ## FFI
 
-We will be using openssl's `MD5` function to do the hashing, so we will need to
-provide a couple of foreign function definitions.
+We will be using openssl's `MD5` function to do the hashing, so we will need to provide a couple of foreign function definitions.
 
-First, we'll provide one for the C standard library's `strlen`. We could get
-this value from within idris, but we'll do it through FFI to flesh out the
-example a bit more.
+First, we'll provide one for the C standard library's `strlen`. We could get this value from within idris, but we'll do it through FFI to flesh out the example a bit more.
 
-The format of the specifier after `%foreign` is "language:function name,library
-name". Since `strlen` is the c standard library, we use `libc` as the library
-name.
+The format of the specifier after `%foreign` is "language:function name,library name". Since `strlen` is the c standard library, we use `libc` as the library name.
 
-Idris will automatically convert primitive types like `String`s and `Int`s to
-their C equivalents at the FFI boundary.
+Idris will automatically convert primitive types like `String`s and `Int`s to their C equivalents at the FFI boundary.
 
-`PrimIO` is a special, basic type of IO action based on linear types, we won't
-be getting into the specifics right now.
+`PrimIO` is a special, basic type of IO action based on linear types, we won't be getting into the specifics right now.
 
 By convention, primitive FFI function names start with `prim__` in idris.
 
@@ -44,12 +36,9 @@ By convention, primitive FFI function names start with `prim__` in idris.
 prim__strlen : String -> PrimIO Int
 ```
 
-Now we need one for the `MD5` function from openssl, the openssl objectfile
-calls itself `libcrypto`, so we'll use that as the library name.
+Now we need one for the `MD5` function from openssl, the openssl objectfile calls itself `libcrypto`, so we'll use that as the library name.
 
-The `MD5` function actually returns a pointer to the hash value, but since the
-3rd argument is the pointer it expects to write the hash to, we already have
-that value and we'll ignore it by having our `prim__md5` return unit.
+The `MD5` function actually returns a pointer to the hash value, but since the 3rd argument is the pointer it expects to write the hash to, we already have that value and we'll ignore it by having our `prim__md5` return unit.
 
 The second argument is the length of the input string in bytes.
 
@@ -58,25 +47,15 @@ The second argument is the length of the input string in bytes.
 prim__md5 : String -> Int -> Ptr Bits8 -> PrimIO ()
 ```
 
-Now we glue these parts together in our higher level `md5'` function.
+Now we glue these parts together in our higher level `md5'` function. 
 
-We use `malloc` from `System.FFI` to allocate a buffer for `prim__md5` to write
-to. This returns an `AnyPtr`, when we need a `Ptr Bits8`, so we'll need to cast
-it, using `prim__castPtr` from the prelude.
+We use `malloc` from `System.FFI` to allocate a buffer for `prim__md5` to write to. This returns an `AnyPtr`, when we need a `Ptr Bits8`, so we'll need to cast it, using `prim__castPtr` from the prelude.
 
-We then use our `prim__strlen` function to get the length of our input string
-from within C, using `primIO` from the prelude to "lift" the resulting
-`PrimIO Int` into our `io` context.
+We then use our `prim__strlen` function to get the length of our input string from within C, using `primIO` from the prelude to "lift" the resulting `PrimIO Int` into our `io` context.
 
-We then feed the string, the calculated length, and our casted buffer into our
-`prim__md5` function, then use `prim__getArrayBits8` from the
-[c-ffi](https://github.com/joelberkeley/c-ffi/) library to extract each of the
-bytes, passing them into a pure idris helper function to convert into hex
-representation.
+We then feed the string, the calculated length, and our casted buffer into our `prim__md5` function, then use `prim__getArrayBits8` from the [c-ffi](https://github.com/joelberkeley/c-ffi/) library to extract each of the bytes, passing them into a pure idris helper function to convert into hex representation.
 
-Since we are working with C FFI and performing a little bit of manual memory
-management here, we must remember to `free` our pointer, and then we can splice
-together our output string and return.
+Since we are working with C FFI and performing a little bit of manual memory management here, we must remember to `free` our pointer, and then we can splice together our output string and return.
 
 ```idris
 md5' : HasIO io => String -> io String
@@ -98,38 +77,21 @@ md5' str = do
       pack [hexDigit (n `shiftR` 4), hexDigit (n .&. 0xF)]
 ```
 
-Now, because foreign functions return a `PrimIO` by default, our `md'` still
-requires some sort of `HasIO` (like IO). This is undesirable here, after all,
-MD5 is a hash function, so it really _ought_ to behave like a pure function. We
-know from taking a careful look at what FFI functions we are invoking that we
-aren't altering any global state.
+Now, because foreign functions return a `PrimIO` by default, our `md'` still requires some sort of `HasIO` (like IO). This is undesirable here, after all, MD5 is a hash function, so it really _ought_ to behave like a pure function. We know from taking a careful look at what FFI functions we are invoking that we aren't altering any global state.
 
-Idris has an escape hatch for these types of situations, `unsafePerformIO`. This
-function is, as the name suggests, _quite_ unsafe, so it shouldn't be used if
-you don't fully understand the implications, and only sparingly at that, but
-doing FFI to C is an intrinsically unsafe operation, so it's morally okay to use
-here, as long as we are careful to not violate referential transparency or type
-safety. Haskell programmers should note that `unsafePerformIO` is _much_ easier
-to use correctly in Idris, largely as a result of Idris being strict by default.
+Idris has an escape hatch for these types of situations, `unsafePerformIO`. This function is, as the name suggests, _quite_ unsafe, so it shouldn't be used if you don't fully understand the implications, and only sparingly at that, but doing FFI to C is an intrinsically unsafe operation, so it's morally okay to use here, as long as we are careful to not violate referential transparency or type safety. Haskell programmers should note that `unsafePerformIO` is _much_ easier to use correctly in Idris, largely as a result of Idris being strict by default.
 
-Finally, we'll construct our top level `md5` function, wrapping `md5'` in
-`unsafePerformIO`
+Finally, we'll construct our top level `md5` function, wrapping `md5'` in `unsafePerformIO`
 
 ```idris
 md5 : String -> String
 md5 str = unsafePerformIO $ md5' str
 ```
-
 ## Solver functions
 
 ### Count the leading zeros in a string
 
-There is a more clever way to do this making use of a "view" strings have for
-interacting with them as if they were lazy lists, but we've already covered so
-much here that we'll save that one for another time and just do it the straight
-forward way, having a top level function that accepts a string, turns it into a
-list of chars, and then pass it into a tail recursive helper function to
-actually count the zeros.
+There is a more clever way to do this making use of a "view" strings have for interacting with them as if they were lazy lists, but we've already covered so much here that we'll save that one for another time and just do it the straight forward way, having a top level function that accepts a string, turns it into a list of chars, and then pass it into a tail recursive helper function to actually count the zeros.
 
 ```idris
 countZeros : String -> Nat
@@ -154,10 +116,7 @@ checkZeros key number =
 
 ### Find the first input with a specific number of zeros
 
-Search numbers starting at the provided seed and counting up in a tail recursive
-helper function. This function is going to be effectively impossible to prove
-totality for, so we have removed our normal `%default total` annotation for this
-file
+Search numbers starting at the provided seed and counting up in a tail recursive helper function. This function is going to be effectively impossible to prove totality for, so we have removed our normal `%default total` annotation for this file
 
 ```idris
 findFirst : (zeros : Nat) -> (key : String) -> (seed : Nat) -> Nat
@@ -171,10 +130,7 @@ findFirst zeros key current =
 
 ### Part 1
 
-Pass the input into our `findFirst` function and use the result as both our
-output and context value. Since part2 is searching for a longer run of 0s than
-part 1, numbers already checked by part 1 can not possibly be valid solutions
-for part 2, so we can skip them in part 2.
+Pass the input into our `findFirst` function and use the result as both our output and context value. Since part2 is searching for a longer run of 0s than part 1, numbers already checked by part 1 can not possibly be valid solutions for part 2, so we can skip them in part 2.
 
 ```idris
 part1 : Eff (PartEff String) (Nat, Nat)
diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md
index d947885..40ed6f0 100644
--- a/src/Years/Y2015/Day5.md
+++ b/src/Years/Y2015/Day5.md
@@ -1,10 +1,6 @@
 # Year 2015 Day 5
 
-This day provides a nice chance to introduce
-[views](https://idris2.readthedocs.io/en/latest/tutorial/views.html),
-specifically `String`'s
-[`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList)
-view, which lets us treat `String`s as if they were lazy lists or iterators.
+This day provides a nice chance to introduce [views](https://idris2.readthedocs.io/en/latest/tutorial/views.html), specifically `String`'s [`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList) view, which lets us treat `String`s as if they were lazy lists or iterators.
 
 <!-- idris
 module Years.Y2015.Day5
@@ -35,39 +31,19 @@ vowels : List Char
 vowels = ['a', 'e', 'i', 'o', 'u']
 ```
 
-Now define a function to check if a string contains a minimum number of vowels.
-Here we make use of the `with` rule and the `AsList` view over strings.
+Now define a function to check if a string contains a minimum number of vowels. Here we make use of the `with` rule and the `AsList` view over strings.
 
-The `with` rule provides dependently typed pattern matching, allowing us to make
-use of the fact that the form of some of the arguments can be determined by the
-values of the others.
+The `with` rule provides dependently typed pattern matching, allowing us to make use of the fact that the form of some of the arguments can be determined by the values of the others. 
 
-The `AsList` view associates a `String` with a lazy list of the characters in
-the string by providing incremental proofs that the `String` decomposes into the
-lazy list. An `AsList` of value `Nil`/`[]` proves that the associated string is
-empty, and an `AsList` of value `c :: xs` proves that the associated string can
-be generated by `strCons`ing the character `c` onto the rest of the string as
-captured by the `AsList` in `xs`.
+The `AsList` view associates a `String` with a lazy list of the characters in the string by providing incremental proofs that the `String` decomposes into the lazy list. An `AsList` of value `Nil`/`[]` proves that the associated string is empty, and an `AsList` of value `c :: xs` proves that the associated string can be generated by `strCons`ing the character `c` onto the rest of the string as captured by the `AsList` in `xs`. 
 
-We use the `asList` function, which generates the `AsList` view for the provided
-string, as the argument to the `with` block. Functions like this that produce
-views for a value are refereed to as "covering functions". In general, views are
-dependently typed constructs whose value provides insight into the structure of
-another value.
+We use the `asList` function, which generates the `AsList` view for the provided string, as the argument to the `with` block. Functions like this that produce views for a value are refereed to as "covering functions". In general, views are dependently typed constructs whose value provides insight into the structure of another value.
 
-We implement this function by keeping a counter of the number of vowels we still
-need to see to accept the string, returning true when that counter equals zero,
-or false if we hit the end of the string (when the string argument is empty and
-the associated `AsList` is `Nil`) while the counter is still non-zero.
+We implement this function by keeping a counter of the number of vowels we still need to see to accept the string, returning true when that counter equals zero, or false if we hit the end of the string (when the string argument is empty and the associated `AsList` is `Nil`) while the counter is still non-zero.
 
-If the counter is non-zero and the string is non-empty, we check the current `c`
-character to see if it is a vowel, by checking to see if our `vowels` list
-contains it, then recurse, decrementing the counter if it was a vowel, and
-leaving the counter unchanged if it wasn't.
+If the counter is non-zero and the string is non-empty, we check the current `c` character to see if it is a vowel, by checking to see if our `vowels` list contains it, then recurse, decrementing the counter if it was a vowel, and leaving the counter unchanged if it wasn't.
 
-The use of `| xs` after the recursive call to `containsVowels` tells Idris to
-recurse directly to the `with` block, allowing it to reuse the `AsList` value in
-`xs` without having to generate the `AsList` view again.
+The use of `| xs` after the recursive call to `containsVowels` tells Idris to recurse directly to the `with` block, allowing it to reuse the `AsList` value in `xs` without having to generate the `AsList` view again. 
 
 ```idris
 containsVowels : (count : Nat) -> String -> Bool
@@ -82,18 +58,11 @@ containsVowels count str with (asList str)
 
 ### At least one letter appears twice in a row
 
-For this one, since we need to inspect two letters at a time, we break out a
-nested `with` block, with the tail of the `AsList` as the argument of the block,
-to also pattern match on the next character of the string.
+For this one, since we need to inspect two letters at a time, we break out a nested `with` block, with the tail of the `AsList` as the argument of the block, to also pattern match on the next character of the string. 
 
-Since the `AsList` view is lazy, we need to use `force` in the inner with block
-to force the evaluation of the next component of the view, this is due to a
-[bug in the compiler](https://github.com/idris-lang/Idris2/issues/3461).
+Since the `AsList` view is lazy, we need to use `force` in the inner with block to force the evaluation of the next component of the view, this is due to a [bug in the compiler](https://github.com/idris-lang/Idris2/issues/3461).
 
-The logic here is pretty simple, if we hit the empty string or get down to one
-character, return `False`, if we have two characters available, compare them,
-returning `True` if they match, and recursing to the outer with block, only
-consuming one of the two characters, if they don't match.
+The logic here is pretty simple, if we hit the empty string or get down to one character, return `False`, if we have two characters available, compare them, returning `True` if they match, and recursing to the outer with block, only consuming one of the two characters, if they don't match.
 
 ```idris
 doubleLetter : String -> Bool
@@ -116,10 +85,7 @@ disallowedSubstrs : List String
 disallowedSubstrs = ["ab", "cd", "pq", "xy"]
 ```
 
-Idris's standard library does not currently define a function to check if a
-string is a substring of another, so we instead use our own `isSubstr` function,
-defined via use of the `AsList` view, from our [Util](../../Util.md#issubstr)
-module.
+Idris's standard library does not currently define a function to check if a string is a substring of another, so we instead use our own `isSubstr` function, defined via use of the `AsList` view, from our [Util](../../Util.md#issubstr) module.
 
 ```idris
 noDisallowed : String -> Bool
@@ -129,8 +95,7 @@ noDisallowed str =
 
 ### isNice
 
-Combine all three of our above functions together to check if a string is a
-"nice" string
+Combine all three of our above functions together to check if a string is a "nice" string
 
 ```idris
 isNice : String -> Bool
@@ -141,9 +106,7 @@ isNice str = containsVowels 3 str && doubleLetter str && noDisallowed str
 
 ### Pair of letters that appears twice
 
-Use a similar approach to `doubleLetter` above, but instead of comparing the two
-chars for equality, pack them into a string and check if they are a substring of
-the rest of the string.
+Use a similar approach to `doubleLetter` above, but instead of comparing the two chars for equality, pack them into a string and check if they are a substring of the rest of the string.
 
 ```idris
 pairTwice : String -> Bool
@@ -159,9 +122,7 @@ pairTwice str with (asList str)
 
 ### Letter that repeats after one letter
 
-More of the same, but this one gets extra fun because we are matching 3 letters
-at a time. This would be a lot nicer if we could get away without nesting the
-`with` blocks, but due to the aformentioned compiler bug, we need the nesting.
+More of the same, but this one gets extra fun because we are matching 3 letters at a time. This would be a lot nicer if we could get away without nesting the `with` blocks, but due to the aformentioned compiler bug, we need the nesting.
 
 ```idris
 letterRepeatGap : String -> Bool
@@ -190,8 +151,7 @@ isNice' str = pairTwice str && letterRepeatGap str
 
 ### Part 1
 
-Split our input up into a list of its component strings, and then count how many
-satisfy the "nice" criteria.
+Split our input up into a list of its component strings, and then count how many satisfy the "nice" criteria.
 
 ```idris
 part1 : Eff (PartEff String) (Nat, ())
diff --git a/src/Years/Y2015/Day6.md b/src/Years/Y2015/Day6.md
index a2b5cd0..cc95926 100644
--- a/src/Years/Y2015/Day6.md
+++ b/src/Years/Y2015/Day6.md
@@ -27,9 +27,7 @@ import Data.IORef
 
 ### Grid structure
 
-Since this is our first 2d grid problem, we'll keep it simple and use a `Vect`
-of `Vect`s to store our problem state, we'll revisit a more complicated but more
-efficient structure for storing a 2d `Grid` in a later problem.
+Since this is our first 2d grid problem, we'll keep it simple and use a `Vect` of `Vect`s to store our problem state, we'll revisit a more complicated but more efficient structure for storing a 2d `Grid` in a later problem.
 
 This alias adds 1 to each of its arguments to ensure non-emptyness.
 
@@ -38,8 +36,7 @@ Grid : (rows, cols : Nat) -> Type -> Type
 Grid rows cols e = Vect (S rows) (Vect (S cols) e)
 ```
 
-We also provide a type alias for the coordinates in this grid, a simple pair of
-`Fin`s.
+We also provide a type alias for the coordinates in this grid, a simple pair of `Fin`s.
 
 ```idris
 Coord : (rows, cols : Nat) -> Type
@@ -96,9 +93,7 @@ Show (Range rows cols) where
 
 Helper function to extract a range of values from our Grid.
 
-First extracts the range of rows this `Range` touches, then maps a an extractor
-for the range of columns it touches across them, before lazily concatenating the
-resulting lists.
+First extracts the range of rows this `Range` touches, then maps a an extractor for the range of columns it touches across them, before lazily concatenating the resulting lists.
 
 ```idris
 extractRange : Range rows cols -> Grid rows cols e -> LazyList e
@@ -123,7 +118,7 @@ Show (Command rows cols) where
     "{\{show action}: \{show range}}"
 -->
 
-### Parsing
+### Parsing 
 
 Pattern match on the action string, throwing an error if the action was invalid
 
@@ -136,8 +131,7 @@ parseAction "toggle" = pure Toggle
 parseAction str = throw "Invalid action: \{str}"
 ```
 
-Attempt to split the string into two parts on the comma, and then attempt to
-parse the parts as `Fin`s, throwing an appropriate error if anything goes wrong
+Attempt to split the string into two parts on the comma, and then attempt to parse the parts as `Fin`s, throwing an appropriate error if anything goes wrong
 
 ```idris
 parseCoord : Has (Except String) fs => 
@@ -163,8 +157,7 @@ parseRange pair1 pair2 = do
   pure $ MkRange top_left bottom_right
 ```
 
-Split a string into a list of parts, pattern matching those parts to attempt to
-extract a `Command`.
+Split a string into a list of parts, pattern matching those parts to attempt to extract a `Command`.
 
 ```idris
 parseCommand : Has (Except String) fs => Has Logger fs =>
@@ -188,10 +181,7 @@ parseCommand input = do
 
 ## Problem structure
 
-Since we are dealing with a million slots here, we'll want some level of true
-mutability. The actual structure containing the slots doesn't need to be
-modified once its setup, so we'll make the mutability interior to the slots and
-keep a `Grid` of `IORef`s.
+Since we are dealing with a million slots here, we'll want some level of true mutability. The actual structure containing the slots doesn't need to be modified once its setup, so we'll make the mutability interior to the slots and keep a `Grid` of `IORef`s.
 
 We'll setup a helper function to initialize our grid based on a seed value.
 
@@ -203,8 +193,7 @@ ioGrid rows cols seed =
   in traverse (traverse id) grid
 ```
 
-Convert a `Grid` of `IORef`s into a `Grid` of pure values by traversing the
-`readIORef` operation over our `Grid`.
+Convert a `Grid` of `IORef`s into a `Grid` of pure values by traversing the `readIORef` operation over our `Grid`.
 
 ```idris
 purify : Has IO fs =>
@@ -219,12 +208,9 @@ purify grid = traverse (traverse readIORef) grid
 ```idris
 namespace Part1
 ```
+Apply a given command to our `Grid` of `IORef`s. 
 
-Apply a given command to our `Grid` of `IORef`s.
-
-Use our `extractRange` function to extract all the `IORef`s in the grid cells
-touched by our `Range` and then traverse an appropriate mutating action over
-them.
+Use our `extractRange` function to extract all the `IORef`s in the grid cells touched by our `Range` and then traverse an appropriate mutating action over them.
 
 ```idris
   applyCommand : Has IO fs =>
@@ -237,8 +223,7 @@ them.
       Toggle => Lazy.traverse_ (`modifyIORef` not) cells
 ```
 
-Apply a list of commands to our `Grid` of `IORef`s, doing some debug logging
-along the way.
+Apply a list of commands to our `Grid` of `IORef`s, doing some debug logging along the way.
 
 ```idris
   export
@@ -261,8 +246,7 @@ along the way.
 namespace Part2
 ```
 
-Much the same as above, but instead we apply the part 2 rules to a `Grid` of
-`Nat`.
+Much the same as above, but instead we apply the part 2 rules to a `Grid` of `Nat`.
 
 ```idris
   applyCommand : Has IO fs =>
@@ -275,9 +259,7 @@ Much the same as above, but instead we apply the part 2 rules to a `Grid` of
       Toggle => Lazy.traverse_ (`modifyIORef` (+ 2)) cells
 ```
 
-Identical to above, except for using our part 2 `applyCommand`. We can use the
-same name here because we have the two variants behind namespaces and Idris can
-disambiguate via the types.
+Identical to above, except for using our part 2 `applyCommand`. We can use the same name here because we have the two variants behind namespaces and Idris can disambiguate via the types.
 
 ```idris
   export
@@ -298,9 +280,7 @@ disambiguate via the types.
 
 ### Part 1
 
-Parse our commands, generate our initial `Grid` with all the lights turned off
-(represented by `False`), apply our commands to it, purify it, and count the
-lights that are turned on.
+Parse our commands, generate our initial `Grid` with all the lights turned off (represented by `False`), apply our commands to it, purify it, and count the lights that are turned on.
 
 Pass out our list of parsed commands as the context for reuse in part 2.
 
@@ -318,9 +298,7 @@ part1 = do
 
 ### Part 2
 
-This time, use an initial `Grid` with all brightness values at 0, apply our list
-of preparsed commands using our part 2 `applyCommands` function (selected via
-the type signature), and then add up the brightnesses.
+This time, use an initial `Grid` with all brightness values at 0, apply our list of preparsed commands using our part 2 `applyCommands` function (selected via the type signature), and then add up the brightnesses.
 
 ```idris
 part2 : List (Command 999 999) -> Eff (PartEff String) Nat
diff --git a/src/Years/Y2015/Day7.md b/src/Years/Y2015/Day7.md
index 5919288..2a8df71 100644
--- a/src/Years/Y2015/Day7.md
+++ b/src/Years/Y2015/Day7.md
@@ -2,16 +2,9 @@
 
 This day provides us a gentle introduction to dependent maps.
 
-Per the problem specification, each wire can only be output to by one gate. To
-encode this property in the type, we'll tag `Gate` with the output wire in the
-type, and then store our ciruct as a dependent map from wires to `Gate`s. This
-ensures that the circut only contains one gate outputting to each wire, and that
-looking up a wire in the ciruct produces exactly the gate that outputs to it
-through type checking.
+Per the problem specification, each wire can only be output to by one gate. To encode this property in the type, we'll tag `Gate` with the output wire in the type, and then store our ciruct as a dependent map from wires to `Gate`s. This ensures that the circut only contains one gate outputting to each wire, and that looking up a wire in the ciruct produces exactly the gate that outputs to it through type checking. 
 
-Ensuring that the input contains only one gate outputting for each wire is done
-through throwing a runtime error in the parsing function if a second gate
-outputting to a given wire is found in the input.
+Ensuring that the input contains only one gate outputting for each wire is done through throwing a runtime error in the parsing function if a second gate outputting to a given wire is found in the input.
 
 <!-- idris
 module Years.Y2015.Day7
@@ -39,8 +32,7 @@ import Decidable.Equality
 
 ### Problem structure
 
-Define type aliases for wires and literals, and specify that an input can be
-either a literal or a wire.
+Define type aliases for wires and literals, and specify that an input can be either a literal or a wire.
 
 ```idris
 Wire : Type 
@@ -136,16 +128,9 @@ parseGate str = do
     _ => throw "Invalid Gate: \{str}"
 ```
 
-Break the input into lines, traverse `parseGate` over the lines, and collect the
-results into our circut DMap.
+Break the input into lines, traverse `parseGate` over the lines, and collect the results into our circut DMap.
 
-The type of a value in a `SortedDMap` depends on the value of the key that
-refers to it, in the type constructor `SortedDMap k v`, `v` is of type
-`k -> Type`, this is the function the map calls to calculate the type of the
-value from the value of the key. This, not so coincidentally, is the type
-signature of our `Gate` type constructor, which we can slot in here to get a map
-from a wire to the gate outputting to that wire, preventing us from accidentally
-associating a wire to the wrong gate.
+The type of a value in a `SortedDMap` depends on the value of the key that refers to it, in the type constructor `SortedDMap k v`, `v` is of type `k -> Type`, this is the function the map calls to calculate the type of the value from the value of the key. This, not so coincidentally, is the type signature of our `Gate` type constructor, which we can slot in here to get a map from a wire to the gate outputting to that wire, preventing us from accidentally associating a wire to the wrong gate.
 
 ```idris
 parseGates : Has (Except String) fs => Has Logger fs => 
@@ -165,8 +150,7 @@ parseGates input = do
 
 ## Solver Functions
 
-Recursively solve for the value on a wire, keeping a cache of already solved
-wires
+Recursively solve for the value on a wire, keeping a cache of already solved wires
 
 ```idris
 covering
@@ -213,10 +197,7 @@ solveWire wire = do
 
 ### Part 1
 
-Parse the input, then feed it and an initial empty cache into our `solveWire`
-function, passing the produced value as the output and the circut, represented
-as a dependent map from wires to gates, as well as the output signal from wire
-'a' as the context for part 2.
+Parse the input, then feed it and an initial empty cache into our `solveWire` function, passing the produced value as the output and the circut, represented as a dependent map from wires to gates, as well as the output signal from wire 'a' as the context for part 2.
 
 ```idris
 covering
@@ -233,8 +214,7 @@ part1 = do
 
 ### Part 2
 
-Override the value for the 'b' wire to the output from the 'a' wire in part 1,
-then rerun our calcuation to find the new output for the 'a' wire.
+Override the value for the 'b' wire to the output from the 'a' wire in part 1, then rerun our calcuation to find the new output for the 'a' wire.
 
 ```idris
 covering
diff --git a/src/Years/Y2015/Day8.md b/src/Years/Y2015/Day8.md
deleted file mode 100644
index daed58e..0000000
--- a/src/Years/Y2015/Day8.md
+++ /dev/null
@@ -1,176 +0,0 @@
-# Year 2015 Day 8
-
-<!-- idris
-module Years.Y2015.Day8
-
-import Control.Eff
-
-import Data.Primitives.Interpolation
-
-import Runner
--->
-
-```idris
-import Data.String
-import Data.Vect
-import Data.Either
-```
-
-## Parsing
-
-Effect alias for a parser
-
-```idris
-Parser : List (Type -> Type)
-Parser =
-  [Choose, State (List Char), Except String]
-```
-
-Get the next character from the state, modifying it in place
-
-```idris
-getNext : Eff Parser Char
-getNext = do
-  chars <- get
-  case chars of 
-    [] => throw "End of Input"
-    (x :: xs) => do
-      put xs
-      pure x
-```
-
-Parse a quote 
-```idris
-quote : Eff Parser ()
-quote = do
-  char <- getNext
-  if char == '"'
-    then pure ()
-    else throw "Expected quote, found: \{show char}"
-```
-
-Parse a char that's not a quote or an escape character
-
-```idris
-normal : Eff Parser Char
-normal = do
-  char <- getNext
-  if any (char ==) (the (List _) ['\\', '"'])
-    then throw "Tried to parse a special character as normal \{show char}"
-    else pure char
-```
-
-Parse a hex digit
-
-```idris
-hexDigit : Eff Parser Int
-hexDigit = do
-  char <- getNext
-  case toLower char of
-    '0' => pure 0x0
-    '1' => pure 0x1
-    '2' => pure 0x2
-    '3' => pure 0x3
-    '4' => pure 0x4
-    '5' => pure 0x5
-    '6' => pure 0x6
-    '7' => pure 0x7
-    '8' => pure 0x8
-    '9' => pure 0x9
-    'a' => pure 0xa
-    'b' => pure 0xb
-    'c' => pure 0xc
-    'd' => pure 0xd
-    'e' => pure 0xe
-    'f' => pure 0xf
-    _ => throw "Invalid hex digit: \{show char}"
-```
-
-Parse an escaped character
-
-```idris
-escaped : Eff Parser Char
-escaped = do 
-  escape <- getNext
-  if escape == '\\'
-    then do
-      first <- getNext
-      case first of
-        '\\' => pure '\\'
-        '"'  => pure '"'
-        'x'  => do
-          [x, y] : Vect _ Int <- sequence [hexDigit, hexDigit]
-          -- Fails to compile 
-          -- pure . chr $ x * 0x10 + y
-          -- Compiles
-          pure . (const 'a') $ x * 0x10 + y
-        _    => throw "Invalid Escape Character: \{show first}"
-    else throw "Tried to parse non escape as escape \{show escape}" 
-```
-
-Parse any non-quote character 
-
-```idris
-character : Eff Parser Char
-character = oneOfM (the (List _) [escaped, normal])
-```
-
-Run a parser until it runs out 
-
-```idris
-parseMany : Eff Parser t -> Eff Parser (List t)
-parseMany x = do
-  Just next <- lift $ catch (\_ => pure Nothing) (map Just x)
-    | _ => pure []
-  map (next ::) (parseMany x)
-```
-
-Parse any number of non-quote characters
-
-```idris
-characters : Eff Parser (List Char)
-characters = parseMany character
-```
-
-Parse a quote delimited string
-
-```idris
-parseString : Eff Parser (List Char)
-parseString = do
-  quote
-  xs <- characters
-  quote
-  pure xs
-```
-
-Run a parser
-
-```idris
-runParser : Eff Parser t -> String -> Maybe t
-runParser m str = 
-  map fst . head' . rights
-  . extract . runChoose {f = List} . runExcept . runState (unpack str) 
-  $ m
-  
-```
-
-## Part Functions
-
-### Part 1
-
-```idris
-part1 : Eff (PartEff String) (Nat, List (List Char, List Char))
-part1 = do
-  inputs <- map (lines . trim) $ askAt "input"
-  let outputs = map (map pack . runParser parseString) inputs
-  let pairs = zip inputs outputs
-  let debug_out = joinBy "\n" . map show $ pairs
-  putStrLn debug_out
-  ?part1_rhs_1
-```
-
-<!-- idris
-public export
-day8 : Day
-day8 = First 8 part1
--->