From dd61600c49bf2d32830c93bbe62169bb0fbf801f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <nathan@mccarty.io>
Date: Sat, 10 Dec 2022 18:17:35 -0500
Subject: [PATCH] Try removing %name to fix highlight

---
 10/Main.idr | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/10/Main.idr b/10/Main.idr
index 83a3ea5..f05ac7c 100644
--- a/10/Main.idr
+++ b/10/Main.idr
@@ -5,7 +5,6 @@ import Data.List
 import System.File.ReadWrite
 
 data Operation = Noop | Addx Int
-%name Operation op
 
 Show Operation where
   show Noop = "Noop"
@@ -27,7 +26,6 @@ parseOps : String -> Maybe (List Operation)
 parseOps str = traverse parseOp (lines str)
 
 data Pixel = On | Off
-%name Pixel pixel
 
 Show Pixel where
   show On = "#"
@@ -39,7 +37,6 @@ record State where
   xRegister : Int
   waitCycles : Nat
   waitingOp : Maybe Operation
-%name State state
 
 Show State where
   show (MkState cycle xRegister waitCycles waitingOp) =
@@ -85,7 +82,6 @@ tickMultiple state ops@(x :: xs) =
 
 data CRT : Type where
   MkCrt : Vect 6 (Vect 40 Pixel) -> CRT
-%name CRT crt
 
 Show CRT where
   show (MkCrt xs) =