rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 14 Pull Requests Releases Wiki Activity

remove some unneeded Ord impls

This commit is contained in:
rhiannon morris 2023-11-30 14:46:45 +01:00
parent f337625801
commit 1c8c50f3e2
1 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
exe/Options.idr
View File

@ -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