diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 1c2bd0f..36c2a5b 100644
--- a/advent-of-code-2024.ipkg
+++ b/advent-of-code-2024.ipkg
@@ -13,10 +13,3 @@ 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 dfbce34..898b247 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -10,3 +10,9 @@ 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 73a5b10..19066b2 100644
--- a/src/Day4/Part1.idr
+++ b/src/Day4/Part1.idr
@@ -1,19 +1,18 @@
 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 = Vect h (Vect w Char)
-
-public export
-Pos : Nat -> Nat -> Type
-Pos h w = (Fin h, Fin w)
+Board h w = Grid h w Char
 
 
 public export
@@ -27,19 +26,10 @@ directions = [U, UR, R, DR, D, DL, L, UL]
 
 export
 parseInput : String -> Maybe (h ** w ** Board h w)
-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)
+parseInput = parseGrid
 
 --- 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
@@ -70,8 +60,8 @@ checkString board str = go (unpack str)
 export
 findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w)
 findChar board c = do
-  i <- toList $ range {len=h}
-  j <- toList $ range {len=w}
+  i <- allFins h
+  j <- allFins w
   guard (index (i, j) board == c)
   pure (i, j)
 
diff --git a/src/Day4/Part2.idr b/src/Day4/Part2.idr
index b8fd9a8..aa95510 100644
--- a/src/Day4/Part2.idr
+++ b/src/Day4/Part2.idr
@@ -4,6 +4,7 @@ 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
new file mode 100644
index 0000000..66ccf64
--- /dev/null
+++ b/src/Day6/Part1.idr
@@ -0,0 +1,95 @@
+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
new file mode 100644
index 0000000..6f25782
--- /dev/null
+++ b/src/Day6/Part2.idr
@@ -0,0 +1,64 @@
+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
new file mode 100644
index 0000000..b644d92
--- /dev/null
+++ b/src/Day7/Part1.idr
@@ -0,0 +1,43 @@
+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
new file mode 100644
index 0000000..9cbe7fe
--- /dev/null
+++ b/src/Day7/Part2.idr
@@ -0,0 +1,21 @@
+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
new file mode 100644
index 0000000..501566f
--- /dev/null
+++ b/src/Day8/Part1.idr
@@ -0,0 +1,57 @@
+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
new file mode 100644
index 0000000..4ca6f60
--- /dev/null
+++ b/src/Day8/Part2.idr
@@ -0,0 +1,49 @@
+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 1902a56..17b048c 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 5 Part2
+latest = Pr 8 Part2
 
 
 solMap : SortedMap Problem (String -> String)
diff --git a/src/Utils.idr b/src/Utils.idr
index 71811a4..d9b51e5 100644
--- a/src/Utils.idr
+++ b/src/Utils.idr
@@ -3,6 +3,7 @@ module Utils
 import Data.Maybe
 import Data.String
 import Data.String.Parser
+import Data.Vect
 
 %default total
 
@@ -28,3 +29,25 @@ 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