From 24285db68678e77bc3c83914b7f7e920a5c47733 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 04:55:07 -0500
Subject: [PATCH] Switch from markdown comments to hidden fences

---
 src/Array.md             |  8 ++++----
 src/Main.md              |  4 ++--
 src/Util.md              | 20 ++++++++++----------
 src/Util/Digits.md       | 16 ++++++++--------
 src/Util/Eff.md          |  4 ++--
 src/Years/Y2015.md       |  4 ++--
 src/Years/Y2015/Day1.md  |  8 ++++----
 src/Years/Y2015/Day10.md | 12 ++++++------
 src/Years/Y2015/Day11.md | 12 ++++++------
 src/Years/Y2015/Day2.md  | 12 ++++++------
 src/Years/Y2015/Day3.md  | 12 ++++++------
 src/Years/Y2015/Day4.md  |  8 ++++----
 src/Years/Y2015/Day5.md  | 12 ++++++------
 src/Years/Y2015/Day6.md  | 24 ++++++++++++------------
 src/Years/Y2015/Day7.md  | 12 ++++++------
 src/Years/Y2015/Day8.md  |  8 ++++----
 src/Years/Y2015/Day9.md  | 12 ++++++------
 17 files changed, 94 insertions(+), 94 deletions(-)

diff --git a/src/Array.md b/src/Array.md
index 98bf078..2721297 100644
--- a/src/Array.md
+++ b/src/Array.md
@@ -12,9 +12,9 @@ import Decidable.Equality
 import Control.WellFounded
 ```
 
-<!-- idris
+```idris hide
 import System
--->
+```
 
 ```idris
 %default total
@@ -89,9 +89,9 @@ Iterable (LazyList a) a where
 
 ## Immutable arrays
 
-<!-- idris
+```idris hide
 namespace Immutable
--->
+```
 
 Immutable arrays created from vectors that provide constant time indexing and
 slicing operations.
diff --git a/src/Main.md b/src/Main.md
index f602362..1d0e2c1 100644
--- a/src/Main.md
+++ b/src/Main.md
@@ -76,7 +76,7 @@ data Error : Type where
 A `Show` implementation for `Error` is provided, hidden in this document for
 brevity.
 
-<!-- idris
+```idris hide
 Show Error where
   show (OptionsError errs) =
     let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
@@ -98,7 +98,7 @@ Show Error where
   show (SolveError year day part err) =
     let err = unlines . map ("  " ++) . lines . show $ err
     in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
--->
+```
 
 ## Extract the year and day
 
diff --git a/src/Util.md b/src/Util.md
index c7a9bbc..4e8de44 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -29,9 +29,9 @@ repeatN (S times') f seed = repeatN times' f (f seed)
 
 ## Either
 
-<!-- idris
+```idris hide
 namespace Either
--->
+```
 
 ### mapLeft
 
@@ -47,9 +47,9 @@ Applies a function to the contents of a `Left` if the value of the given
 
 ## List
 
-<!-- idris 
+```idris hide
 namespace List
--->
+```
 
 ### contains
 
@@ -94,12 +94,12 @@ Define some operations for pairs of numbers, treating them roughly like vectors
 
 ### Addition and Subtraction
 
-<!-- idris
+```idris hide
 export infixl 8 >+<
 export infixl 8 >-<
 
 namespace Pair
--->
+```
 
 ```idris
   public export
@@ -115,9 +115,9 @@ namespace Pair
 
 Extend `Data.SortedSet`
 
-<!-- idris
+```idris hide
 namespace Set
--->
+```
 
 ### length
 
@@ -133,9 +133,9 @@ Count the number of elements in a sorted set
 
 Extend `Data.String`
 
-<!-- idris
+```idris hide
 namespace String
--->
+```
 
 ### isSubstr
 
diff --git a/src/Util/Digits.md b/src/Util/Digits.md
index 4cf58b0..6609c6c 100644
--- a/src/Util/Digits.md
+++ b/src/Util/Digits.md
@@ -6,11 +6,11 @@ module Util.Digits
 import Data.Monoid.Exponentiation
 ```
 
-<!-- idris
+```idris hide
 import System
 
 %default total
--->
+```
 
 This module provides views and associated functionality for treating `Integers`
 as if they were lists of numbers.
@@ -22,10 +22,10 @@ teaching purposes, we'll do it here, but please consider a library like
 [prim](https://github.com/stefan-hoeck/idris2-prim) if you find yourself needing
 to prove properties about primitive types.
 
-<!-- idris
+```idris hide
 -- This mutual block isn't strictly required, but is useful for literate purposes
 mutual
--->
+```
 
 ## Primitive functionality
 
@@ -50,14 +50,14 @@ most significant digit.
 
 For a clarifying example:
 
-<!-- idris
+```idris hide
   -- @@test Ascending Digits Example
   ascendingExample : IO Bool
   ascendingExample = do
     putStrLn "Expecting: \{show [5, 4, 3, 2, 1]}"
     putStrLn "Got: \{show . ascList $ ascending 12345}"
     pure $
--->
+```
 
 ```idris
     ascList (ascending 12345) == [5, 4, 3, 2, 1]
@@ -121,14 +121,14 @@ least significant digit.
 
 For a clarifying example:
 
-<!-- idris
+```idris hide
   -- @@test Descending Digits Example
   descendingExample : IO Bool
   descendingExample = do
     putStrLn "Expecting: \{show [1, 2, 3, 4, 5]}"
     putStrLn "Got: \{show . decList $ descending 12345}"
     pure $
--->
+```
 
 ```idris
     decList (descending 12345) == [1, 2, 3, 4, 5]
diff --git a/src/Util/Eff.md b/src/Util/Eff.md
index 1baa453..8441eb9 100644
--- a/src/Util/Eff.md
+++ b/src/Util/Eff.md
@@ -36,7 +36,7 @@ data Level : Type where
   Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
 ```
 
-<!-- idris
+```idris hide
 export
 levelToNat : Level -> Nat
 levelToNat Err = 0
@@ -67,7 +67,7 @@ export infixl 8 >+
 export
 (>+) : Level -> Nat -> Level
 (>+) x k = natToLevel (k + levelToNat x)
--->
+```
 
 Convert a `Level` into a colorized tag
 
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index f745517..c2a0326 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -6,7 +6,7 @@ import Structures.Dependent.FreshList
 import Runner
 ```
 
-<!-- idris
+```idris hide
 import Years.Y2015.Day1
 import Years.Y2015.Day2
 import Years.Y2015.Day3
@@ -18,7 +18,7 @@ import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
--->
+```
 
 # Days
 
diff --git a/src/Years/Y2015/Day1.md b/src/Years/Y2015/Day1.md
index f8820d3..49369d9 100644
--- a/src/Years/Y2015/Day1.md
+++ b/src/Years/Y2015/Day1.md
@@ -3,7 +3,7 @@
 Pretty simple, basic warmup problem, nothing really novel is on display here
 except the effectful part computations.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day1
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Runner
 
 %default total
--->
+```
 
 ## Solver Functions
 
@@ -76,8 +76,8 @@ part2 x = do
   pure $ findBasement 1 0 input
 ```
 
-<!-- idris
+```idris hide
 public export
 day1 : Day
 day1 = Both 1 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day10.md b/src/Years/Y2015/Day10.md
index 201e0c5..d07edf8 100644
--- a/src/Years/Y2015/Day10.md
+++ b/src/Years/Y2015/Day10.md
@@ -3,13 +3,13 @@
 This day doesn't really add anything new, but we will show off our new views for
 viewing integers as lists of digits.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day10
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -22,9 +22,9 @@ import Util
 import Util.Digits
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 # Solver Functions
 
@@ -118,8 +118,8 @@ part2 digits = do
   pure $ count (const True) output
 ```
 
-<!-- idris
+```idris hide
 public export
 day10 : Day
 day10 = Both 10 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day11.md b/src/Years/Y2015/Day11.md
index 43d7908..e034152 100644
--- a/src/Years/Y2015/Day11.md
+++ b/src/Years/Y2015/Day11.md
@@ -10,13 +10,13 @@ implement the one we need for today's task as a throw away data structure just
 for this module, we will be using the `refined`[^1] library's implementation for
 the sake of getting on with it.
 
-<!-- idris 
+```idris hide
 module Years.Y2015.Day11
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Vect
@@ -55,13 +55,13 @@ record PasswordChar where
 %name PasswordChar pc
 ```
 
-<!-- idris
+```idris hide
 Show PasswordChar where
   show (MkPC char) = singleton char
 
 Eq PasswordChar where
   x == y = x.char == y.char
--->
+```
 
 A function to fallible convert `Char`s into refined `PasswordChar`s, this will
 return `Just` if the `Char` satisfies the predicate, and `Nothing` otherwise,
@@ -227,11 +227,11 @@ part2 password = do
   pure $ passwordToString next_password
 ```
 
-<!-- idris
+```idris hide
 public export
 day11 : Day
 day11 = Both 11 part1 part2
--->
+```
 
 ## References
 
diff --git a/src/Years/Y2015/Day2.md b/src/Years/Y2015/Day2.md
index 22081b2..9ab3ead 100644
--- a/src/Years/Y2015/Day2.md
+++ b/src/Years/Y2015/Day2.md
@@ -2,13 +2,13 @@
 
 This day provides us our first little taste of effectful parsing
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day2
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.List
@@ -16,9 +16,9 @@ import Data.List1
 import Data.String
 ```
 
-<!-- idris 
+```idris hide
 %default total
--->
+```
 
 ## Box structure
 
@@ -130,8 +130,8 @@ part2 : (boxes : List Box) -> Eff (PartEff String) Integer
 part2 boxes = pure . sum . map totalRibbon $ boxes
 ```
 
-<!-- idris
+```idris hide
 public export
 day2 : Day
 day2 = Both 2 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md
index 195d1d9..daa922d 100644
--- a/src/Years/Y2015/Day3.md
+++ b/src/Years/Y2015/Day3.md
@@ -3,13 +3,13 @@
 This day provides a gentle introduction to `mutual` blocks and mutually
 recursive functions.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day3
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.SortedSet
@@ -18,9 +18,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -152,8 +152,8 @@ part2 movements = do
   pure . length $ locations
 ```
 
-<!-- idris
+```idris hide
 public export
 day3 : Day
 day3 = Both 3 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day4.md b/src/Years/Y2015/Day4.md
index f907fa1..78d0abe 100644
--- a/src/Years/Y2015/Day4.md
+++ b/src/Years/Y2015/Day4.md
@@ -3,13 +3,13 @@
 This day introduces us to a little bit of FFI, linking to openssl to use it's
 `MD5` functionality.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day4
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -196,8 +196,8 @@ part2 seed = do
   pure number
 ```
 
-<!-- idris
+```idris hide
 public export
 day4 : Day
 day4 = Both 4 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md
index e41bd96..d1b3ccb 100644
--- a/src/Years/Y2015/Day5.md
+++ b/src/Years/Y2015/Day5.md
@@ -6,13 +6,13 @@ 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
+```idris hide
 module Years.Y2015.Day5
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -20,9 +20,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Nice Strings
 
@@ -213,8 +213,8 @@ part2 _ = do
   pure x
 ```
 
-<!-- idris
+```idris hide
 public export
 day5 : Day
 day5 = Both 5 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day6.md b/src/Years/Y2015/Day6.md
index bc5f116..c15596d 100644
--- a/src/Years/Y2015/Day6.md
+++ b/src/Years/Y2015/Day6.md
@@ -2,13 +2,13 @@
 
 Introduction to the advent of code classic 2d grid problem.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day6
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Util
@@ -21,9 +21,9 @@ import Data.String
 import Data.IORef
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -75,12 +75,12 @@ The three types of action that can be performed on a light.
 data Action = On | Off | Toggle
 ```
 
-<!-- idris
+```idris hide
 Show Action where
   show On = "on"
   show Off = "off"
   show Toggle = "toggle"
--->
+```
 
 The range of coordinates that a command affects
 
@@ -90,11 +90,11 @@ record Range (rows, cols : Nat) where
   top_left, bottom_right : Coord rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Range rows cols) where
   show (MkRange top_left bottom_right) = 
     "\{show top_left} -> \{show bottom_right}"
--->
+```
 
 Helper function to extract a range of values from our Grid.
 
@@ -119,11 +119,11 @@ record Command (rows, cols : Nat) where
   range : Range rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Command rows cols) where
   show (MkCmd action range) = 
     "{\{show action}: \{show range}}"
--->
+```
 
 ### Parsing
 
@@ -334,8 +334,8 @@ part2 commands = do
   pure brightness
 ```
 
-<!-- idris
+```idris hide
 public export
 day6 : Day
 day6 = Both 6 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day7.md b/src/Years/Y2015/Day7.md
index 2eafd70..9e663f6 100644
--- a/src/Years/Y2015/Day7.md
+++ b/src/Years/Y2015/Day7.md
@@ -13,13 +13,13 @@ 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
+```idris hide
 module Years.Y2015.Day7
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Bits
@@ -31,9 +31,9 @@ import Data.SortedMap.Dependent
 import Decidable.Equality
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -252,8 +252,8 @@ part2 (circut, value) = do
   pure value
 ```
 
-<!-- idris
+```idris hide
 public export covering
 day7 : Day
 day7 = Both 7 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day8.md b/src/Years/Y2015/Day8.md
index 6b285b9..621cae2 100644
--- a/src/Years/Y2015/Day8.md
+++ b/src/Years/Y2015/Day8.md
@@ -3,7 +3,7 @@
 This day provides a more in depth introduction to writing effectful parsers,
 making use of state and non-determinism in our parsers.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day8
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Data.Primitives.Interpolation
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -344,8 +344,8 @@ part2 inputs = do
   pure difference
 ```
 
-<!-- idris
+```idris hide
 public export
 day8 : Day
 day8 = Both 8 part1 part2
--->
+```
diff --git a/src/Years/Y2015/Day9.md b/src/Years/Y2015/Day9.md
index c689b78..d30a9b0 100644
--- a/src/Years/Y2015/Day9.md
+++ b/src/Years/Y2015/Day9.md
@@ -6,13 +6,13 @@ meeting the problem criteria, and then figure out the length in a separate step.
 This isn't a particularly efficient solution, but its good enough for this small
 problem size.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day9
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -70,10 +70,10 @@ DistanceMap : Type
 DistanceMap = SortedMap Location (List LP)
 ```
 
-<!-- idris
+```idris hide
 Show l => Show (LocationPair l) where
   show (MkLP [x, y] distance) = "\{show x} <-> \{show y}: \{show distance}"
--->
+```
 
 Perform simple, pattern matching based parsing of a location pair.
 
@@ -287,8 +287,8 @@ part2 (distance_map, pairs) = do
   pure len
 ```
 
-<!-- idris
+```idris hide
 public export
 day9 : Day
 day9 = Both 9 part1 part2
--->
+```