Switch from markdown comments to hidden fences

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.

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
 

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
 

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]

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
 

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
 

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
--->
+```

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
--->
+```

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
 

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
--->
+```

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
--->
+```

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
--->
+```

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
--->
+```

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
--->
+```

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
--->
+```

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
--->
+```

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
--->
+```