diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 36c2a5b..1c2bd0f 100644
--- a/advent-of-code-2024.ipkg
+++ b/advent-of-code-2024.ipkg
@@ -13,3 +13,10 @@ depends = contrib
 
 executable = advent-of-code-2024
 main = Main
+modules = Main, Utils, AllDays,
+          Data.Problem,
+          Day1.Part1, Day1.Part2,
+          Day2.Part1, Day2.Part2,
+          Day3.Part1, Day3.Part2,
+          Day4.Part1, Day4.Part2,
+          Day5.Part1, Day5.Part2
diff --git a/src/AllDays.idr b/src/AllDays.idr
index 898b247..dfbce34 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -10,9 +10,3 @@ import public Day4.Part1
 import public Day4.Part2
 import public Day5.Part1
 import public Day5.Part2
-import public Day6.Part1
-import public Day6.Part2
-import public Day7.Part1
-import public Day7.Part2
-import public Day8.Part1
-import public Day8.Part2
diff --git a/src/Day4/Part1.idr b/src/Day4/Part1.idr
index 19066b2..73a5b10 100644
--- a/src/Day4/Part1.idr
+++ b/src/Day4/Part1.idr
@@ -1,18 +1,19 @@
 module Day4.Part1
 
-import Data.List
 import Data.String
 import Data.Vect
 
-import Utils
-
 %default total
 
 --- TYPES
 
 public export
 Board : Nat -> Nat -> Type
-Board h w = Grid h w Char
+Board h w = Vect h (Vect w Char)
+
+public export
+Pos : Nat -> Nat -> Type
+Pos h w = (Fin h, Fin w)
 
 
 public export
@@ -26,10 +27,19 @@ directions = [U, UR, R, DR, D, DL, L, UL]
 
 export
 parseInput : String -> Maybe (h ** w ** Board h w)
-parseInput = parseGrid
+parseInput inp =
+  let ls@(row :: _) = unpack <$> lines inp
+        | [] => Just (0 ** 0 ** [])
+      width = length row
+  in map (\l => (length l ** width ** fromList l))
+       (traverse (toVect width) ls)
 
 --- DATA
 
+export
+index : Pos h w -> Board h w -> Char
+index (i, j) = index j . index i
+
 predFin : Fin n -> Maybe (Fin n)
 predFin FZ = Nothing
 predFin (FS x) = Just $ weaken x
@@ -60,8 +70,8 @@ checkString board str = go (unpack str)
 export
 findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w)
 findChar board c = do
-  i <- allFins h
-  j <- allFins w
+  i <- toList $ range {len=h}
+  j <- toList $ range {len=w}
   guard (index (i, j) board == c)
   pure (i, j)
 
diff --git a/src/Day4/Part2.idr b/src/Day4/Part2.idr
index aa95510..b8fd9a8 100644
--- a/src/Day4/Part2.idr
+++ b/src/Day4/Part2.idr
@@ -4,7 +4,6 @@ import Data.String
 import Data.Vect
 
 import Day4.Part1
-import Utils
 
 %default total
 
diff --git a/src/Day6/Part1.idr b/src/Day6/Part1.idr
deleted file mode 100644
index 66ccf64..0000000
--- a/src/Day6/Part1.idr
+++ /dev/null
@@ -1,95 +0,0 @@
-module Day6.Part1
-
-import Data.Colist
-import Data.List
-import Data.Maybe
-import Data.Vect
-import Data.Vect.Quantifiers
-
-import Utils
-
-%default total
-
---- TYPES
-
-public export
-data Direction = U | R | D | L
-
-export
-Eq Direction where
-  U == U = True
-  D == D = True
-  L == L = True
-  R == R = True
-  _ == _ = False
-
--- True if there is an obstacle
-public export
-Map : Nat -> Nat -> Type
-Map h w = Grid h w Bool
-
---- PARSING
-
-parseDir : Char -> Maybe Direction
-parseDir '^' = Just U
-parseDir '>' = Just R
-parseDir 'v' = Just D
-parseDir '<' = Just L
-parseDir _ = Nothing
-
-export
-parseInput : String -> Maybe (h ** w ** (Map h w, Pos h w, Direction))
-parseInput inp = do
-  (h ** w ** grid) <- parseGrid inp
-  g <- findGuard grid
-  pure (h ** w ** ((map . map) (=='#') grid, g))
-  where
-    findGuard : Vect h (Vect w Char) -> Maybe (Pos h w, Direction)
-    findGuard [] = Nothing
-    findGuard (row :: vs) =
-      case any (\c => isItJust (parseDir c)) row of
-        Yes p => Just ((FZ, cast $ anyToFin p), fromJust _ @{anyToFinCorrect p})
-        No _ => map (mapFst (mapFst FS)) $ findGuard vs
-
---- DATA
-
-predFin : Fin n -> Maybe (Fin n)
-predFin FZ = Nothing
-predFin (FS x) = Just $ weaken x
-
-export
-moveDir : {h, w : _} -> Direction -> Pos h w -> Maybe (Pos h w)
-moveDir U (i, j) = (,j) <$> predFin i
-moveDir R (i, j) = (i,) <$> strengthen (FS j)
-moveDir D (i, j) = (,j) <$> strengthen (FS i)
-moveDir L (i, j) = (i,) <$> predFin j
-
-export
-rotate : Direction -> Direction
-rotate U = R
-rotate R = D
-rotate D = L
-rotate L = U
-
-getRoute : {h, w : _} -> (Pos h w, Direction) -> Map h w
-            -> Colist (Pos h w, Direction)
-getRoute (pos, dir) mp =
-  let Just next = moveDir dir pos
-        | Nothing => [(pos, dir)]
-  in (pos, dir) ::
-      if index next mp
-      then getRoute (pos, rotate dir) mp
-      else getRoute (next, dir) mp
-
---- SOLUTION
-
-covering
-forceList : Colist a -> List a
-forceList [] = []
-forceList (x :: xs) = x :: forceList xs
-
-export covering
-solution : String -> Maybe Nat
-solution inp = do
-  (h ** w ** (mp, g)) <- parseInput inp
-  pure $ length $ nub $ map fst $ forceList $ getRoute g mp
diff --git a/src/Day6/Part2.idr b/src/Day6/Part2.idr
deleted file mode 100644
index 6f25782..0000000
--- a/src/Day6/Part2.idr
+++ /dev/null
@@ -1,64 +0,0 @@
-module Day6.Part2
-
-import Data.Colist
-import Data.List
-import Data.Maybe
-import Data.Vect
-
-import Day6.Part1
-import Utils
-
-%default total
-
---- DATA
-
-getCollisions : {h, w : _} -> (Pos h w, Direction) -> Map h w
-            -> Colist (Pos h w, Direction)
-getCollisions (pos, dir) mp =
-  let Just next = moveDir dir pos
-        | Nothing => []
-  in if index next mp
-      then (next, dir) :: getCollisions (pos, rotate dir) mp
-      else assert_total $ getCollisions (next, dir) mp
-
-insertObs : Pos h w -> Map h w -> Map h w
-insertObs (i, j) = updateAt i (replaceAt j True)
-
--- Must be total, as element type is finite
-checkRepeated : Colist (Pos h w, Direction) -> Bool
-checkRepeated = assert_total $ go []
-  where
-    covering
-    go : Eq a => List a -> Colist a -> Bool
-    go _ [] = False
-    go seen (x :: xs) =
-      (x `elem` seen) || go (x :: seen) xs
-
-covering
-loopPos : {h, w : _} -> (Pos h w, Direction) -> Map h w
-          -> List (Pos h w)
-loopPos g mp = do
-  i <- allFins h
-  j <- allFins w
-  let obs = (i,j)
-  guard (obs /= fst g && not (index obs mp)) -- must be empty space
-  let cols = getCollisions g $ insertObs obs mp
-  guard (collides obs cols) -- guard must collide with obstacle
-  guard (checkRepeated cols) -- must cause a loop
-  pure obs
-  where
-    -- Total in practice because routes that don't hit the new obstacle should
-    -- be finite, but we can't assume that from user input, so mark as covering
-    covering
-    collides : Pos h w -> Colist (Pos h w, Direction) -> Bool
-    collides _ [] = False
-    collides obs ((pos, _) :: cols) =
-      pos == obs || collides obs cols
-
---- SOLUTION
-
-export covering
-solution : String -> Maybe Nat
-solution inp = do
-  (h ** w ** (mp, g)) <- parseInput inp
-  pure $ length $ loopPos g mp
diff --git a/src/Day7/Part1.idr b/src/Day7/Part1.idr
deleted file mode 100644
index b644d92..0000000
--- a/src/Day7/Part1.idr
+++ /dev/null
@@ -1,43 +0,0 @@
-module Day7.Part1
-
-import Data.List1
-import Data.String
-
-import Utils
-
-%default total
-
---- TYPES
-
-public export
-Op : Type
-Op = Nat -> Nat -> Nat
-
---- PARSING
-
-parseLine : String -> Maybe (Nat, List1 Nat)
-parseLine inp =
-  let (part1 ::: [part2]) = split (==':') inp
-        | _ => Nothing
-  in (,) <$> parseNat part1
-         <*> (traverse parseNat =<< fromList (words part2))
-
-export
-parseInput : String -> Maybe (List (Nat, List1 Nat))
-parseInput = traverse parseLine . lines
-
---- DATA
-
-export
-search : List Op -> (tg, tot : Nat) -> List Nat -> Bool
-search _ tg tot [] = tg == tot
-search ops tg tot (x :: xs) =
-  -- heuristic: abandon if running total is larger than target
-  tot <= tg && any (\op => search ops tg (op tot x) xs) ops
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution = map (sum . map fst . filter (\(tg,x:::xs) => search [(+),(*)] tg x xs))
-           . parseInput
diff --git a/src/Day7/Part2.idr b/src/Day7/Part2.idr
deleted file mode 100644
index 9cbe7fe..0000000
--- a/src/Day7/Part2.idr
+++ /dev/null
@@ -1,21 +0,0 @@
-module Day7.Part2
-
-import Data.List1
-
-import Day7.Part1
-import Utils
-
-%default total
-
---- DATA
-
-concat : Nat -> Nat -> Nat
-concat x y = cast $ show x ++ show y
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution = map (sum . map fst
-                    . filter (\(tg,x:::xs) => search [(+),(*),concat] tg x xs))
-           . parseInput
diff --git a/src/Day8/Part1.idr b/src/Day8/Part1.idr
deleted file mode 100644
index 501566f..0000000
--- a/src/Day8/Part1.idr
+++ /dev/null
@@ -1,57 +0,0 @@
-module Day8.Part1
-
-import Data.List
-import Data.Vect
-
-import Utils
-
-%default total
-
---- TYPES
-
-public export
-Map : (h, w : Nat) -> Type
-Map h w = Grid h w (Maybe Char)
-
---- PARSING
-
-export
-parseInput : String -> Maybe (h ** w ** Map h w)
-parseInput inp = do
-  (h ** w ** grid) <- parseGrid inp
-  pure (h ** w ** map (map (filter (/='.') . Just)) grid)
-
---- DATA
-
-export
-frequencies : Map h w -> List Char
-frequencies mp = nub $ do
-  row <- toList mp
-  Just c <- toList row
-    | Nothing => empty
-  pure c
-
-antinodePos : {h, w : _} -> (a, b : Pos h w) -> Maybe (Pos h w)
-antinodePos (x, y) (x', y') =
-  (,) <$> integerToFin (cast x * 2 - cast x') h
-      <*> integerToFin (cast y * 2 - cast y') w
-
-antinodes : {h, w : _} -> Map h w -> Char -> List (Pos h w)
-antinodes mp c = do
-  let poss = do
-        i <- allFins h
-        j <- allFins w
-        guard (index (i, j) mp == Just c)
-        pure (i, j)
-  p1 <- poss
-  p2 <- poss
-  guard (p1 /= p2)
-  toList (antinodePos p1 p2) <|> toList (antinodePos p2 p1)
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution inp = do
-  (h ** w ** mp) <- parseInput inp
-  pure $ length $ nub $ frequencies mp >>= antinodes mp
diff --git a/src/Day8/Part2.idr b/src/Day8/Part2.idr
deleted file mode 100644
index 4ca6f60..0000000
--- a/src/Day8/Part2.idr
+++ /dev/null
@@ -1,49 +0,0 @@
-module Day8.Part2
-
-import Data.List
-import Data.Vect
-
-import Day8.Part1
-import Utils
-
-%default total
-
---- DATA
-
-antinodePos : {h, w : _} -> (a, b : Pos h w) -> List (Pos h w)
-antinodePos (x, y) (x', y') = do
-  let dx = cast x' - cast x
-      dy = cast y' - cast y
-      (dx', dy') = reduce (dx, dy)
-  n <- [-(cast $ max h w)..(cast $ max h w)]
-  toList $
-    (,) <$> integerToFin (cast x + dx' * n) h
-        <*> integerToFin (cast y + dy' * n) w
-  where
-    reduce : (Integer, Integer) -> (Integer, Integer)
-    reduce (a, b) with (cast {to=Nat} $ abs a) | (cast {to=Nat} $ abs b)
-      _ | Z | _ = (a, b)
-      _ | _ | Z = (a, b)
-      _ | a'@(S _) | b'@(S _) =
-        let g = assert_total $ gcd a' b'
-        in (a `div` cast g, b `div` cast g)
-
-antinodes : {h, w : _} -> Map h w -> Char -> List (Pos h w)
-antinodes mp c = do
-  let poss = do
-        i <- allFins h
-        j <- allFins w
-        guard (index (i, j) mp == Just c)
-        pure (i, j)
-  p1 <- poss
-  p2 <- poss
-  guard (p1 /= p2)
-  antinodePos p1 p2
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution inp = do
-  (h ** w ** mp) <- parseInput inp
-  pure $ length $ nub $ frequencies mp >>= antinodes mp
diff --git a/src/Main.idr b/src/Main.idr
index 17b048c..1902a56 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -13,7 +13,7 @@ import AllDays
 ||| The latest problem that has been solved.
 -- NOTE: UPDATE AFTER EACH SOLUTION
 latest : Problem
-latest = Pr 8 Part2
+latest = Pr 5 Part2
 
 
 solMap : SortedMap Problem (String -> String)
diff --git a/src/Utils.idr b/src/Utils.idr
index d9b51e5..71811a4 100644
--- a/src/Utils.idr
+++ b/src/Utils.idr
@@ -3,7 +3,6 @@ module Utils
 import Data.Maybe
 import Data.String
 import Data.String.Parser
-import Data.Vect
 
 %default total
 
@@ -29,25 +28,3 @@ scan p = until p *> p
 export covering
 scanWhile : Monad m => ParseT m a -> ParseT m b -> ParseT m b
 scanWhile w p = many (lookahead w *> requireFailure p *> skip (satisfy (const True))) *> p
-
-
-public export
-Grid : (h, w : Nat) -> Type -> Type
-Grid h w a = Vect h (Vect w a)
-
-public export
-Pos : (h, w : Nat) -> Type
-Pos h w = (Fin h, Fin w)
-
-export
-parseGrid : String -> Maybe (h ** w ** Grid h w Char)
-parseGrid str =
-  let ls@(row :: _) = unpack <$> lines str
-        | [] => Just (0 ** 0 ** [])
-      width = length row
-  in map (\l => (length l ** width ** fromList l))
-       (traverse (toVect width) ls)
-
-export
-index : Pos h w -> Grid h w a -> a
-index (i, j) = index j . index i