21 lines
512 B
Idris
21 lines
512 B
Idris
module Quox.PrettyValExtra
|
|
|
|
import Data.DPair
|
|
import Derive.Prelude
|
|
import public Text.Show.Value
|
|
import public Text.Show.PrettyVal
|
|
import public Text.Show.PrettyVal.Derive
|
|
|
|
%language ElabReflection
|
|
|
|
%runElab derive "SnocList" [PrettyVal]
|
|
|
|
|
|
export %inline
|
|
PrettyVal a => PrettyVal (Subset a p) where
|
|
prettyVal (Element x _) = Con "Element" [prettyVal x, Con "_" []]
|
|
|
|
export %inline
|
|
(forall x. PrettyVal (p x)) => PrettyVal (Exists p) where
|
|
prettyVal (Evidence _ p) = Con "Evidence" [Con "_" [], prettyVal p]
|