From 1c8c50f3e23dcd8988c6d629557b20e751fedd9f Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 30 Nov 2023 14:46:45 +0100 Subject: [PATCH] remove some unneeded Ord impls --- exe/Options.idr | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/exe/Options.idr b/exe/Options.idr index 256bca5..1c444e2 100644 --- a/exe/Options.idr +++ b/exe/Options.idr @@ -13,25 +13,24 @@ import Derive.Prelude public export data OutFile = File String | Console | NoOut %name OutFile f -%runElab derive "OutFile" [Eq, Ord, Show] +%runElab derive "OutFile" [Eq, Show] public export data Phase = Parse | Check | Erase | Scheme | End %name Phase p -%runElab derive "Phase" [Eq, Ord, Show] +%runElab derive "Phase" [Eq, Show] ||| a list of all intermediate `Phase`s (excluding `End`) public export %inline allPhases : List Phase allPhases = %runElab do - -- as a script so it stays up to date cs <- getCons $ fst !(lookupName "Phase") traverse (check . var) $ fromMaybe [] $ init' cs ||| `Guess` is `Term` for a terminal and `NoHL` for a file public export data HLType = Guess | NoHL | Term | Html -%runElab derive "HLType" [Eq, Ord, Show] +%runElab derive "HLType" [Eq, Show] public export record Dump where