General revisions, improve README

README.md

@@ -4,7 +4,22 @@ 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
+## Authors Note
+
+The solutions contained in this project are intended to be read in sequential
+order, though can reasonably be read in any order if you have a good level of
+familiarity with more advanced functional programming topics.
+
+The solutions will involve progressively more advanced topics as day and year
+number increase, though I try not to introduce too much within the scope of any
+one day.
+
+Suggestions and other feedback are highly welcome, please reach out to me via
+any platform you know me on, or send an email to the
+[~thatonelutenist/public-inbox](https://lists.sr.ht/~thatonelutenist/public-inbox)
+mailing list on source hut.
+
+## Index of non-day modules
 
 - [Runner](src/Runner.md)
 
@@ -31,17 +46,56 @@ solution.
     Provide views that enable recursively pattern matching numbers as lists of
     digits, in both ascending and descending order of significance.
 
-# Index of years and days
+## Index of years and days
 
 - 2015
   - [Day 1](src/Years/Y2015/Day1.md)
+
+    Warm up problem, breaks in our new runner and not much else interesting.
+
   - [Day 2](src/Years/Y2015/Day2.md)
+
+    An early hint of effectful parsing.
+
   - [Day 3](src/Years/Y2015/Day3.md)
+
+    Peculiarities of writing mutually recursive functions in dependently typed
+    languages.
+
   - [Day 4](src/Years/Y2015/Day4.md)
+
+    Basic FFI to openssl to steal its MD5 function for Idris's use.
+
   - [Day 5](src/Years/Y2015/Day5.md)
+
+    First introduction to views and dependent pattern matching[^1].
+
   - [Day 6](src/Years/Y2015/Day6.md)
+
+    Naive approach to handling the first 2d grid problem.
+
   - [Day 7](src/Years/Y2015/Day7.md)
+
+    Introduces dependent maps and indexed type families.
+
   - [Day 8](src/Years/Y2015/Day8.md)
+
+    Proper effectful parsers and non-determinism in effect stacks.
+
   - [Day 9](src/Years/Y2015/Day9.md)
+
+    Naive approach to handling the first graph traversal problem.
+
   - [Day 10](src/Years/Y2015/Day10.md)
+
+    Introduce our `Digits`, dependent pattern matching on integers as lists of
+    digits.
+
   - [Day 11](src/Years/Y2015/Day11.md)
+
+    Introduces refinement types
+
+## References
+
+[^1]: Idris 2 Manual:
+    [Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule)

src/Years/Y2015/Day6.md

@@ -1,4 +1,8 @@
-# [Year 2015 Day 6](https://adventofcode.com/2015/day/6)
+# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/
+
+6.
+
+Introduction to the advent of code classic 2d grid problem.
 
 <!-- idris
 module Years.Y2015.Day6

src/Years/Y2015/Day7.md

@@ -1,4 +1,6 @@
-# [Year 2015 Day 7](https://adventofcode.com/2015/day/7)
+# \[Year 2015 Day 7\](https://adventofcode.com/2015/day/
+
+7.
 
 This day provides us a gentle introduction to dependent maps.
 
@@ -53,7 +55,10 @@ Input : Type
 Input = Either Literal Wire
 ```
 
-Description of a Gate, tagged in the type with the name of the output wire
+Description of a Gate, tagged in the type with the name of the output wire.
+
+This creates what is referred to as an "indexed type family", in this case a
+family of `Gate` types indexed by values of type `Wire`.
 
 ```idris
 data Gate : Wire -> Type where