0 | module Data.DShow
 1 |
 2 | ||| Equivalent of `Show` for single-parameter dependent types
 3 | |||
 4 | ||| Inspired by the `GShow` typeclass from Haskells "some" package.
 5 | ||| Modeled after the `Show` interface from `base`.
 6 | public export
 7 | interface DShow (0 f : t -> Type) where
 8 |
 9 |   ||| Analogous to `show`
10 |   dshow : f a -> String
11 |   dshow x = dshowPrec {f} Open x
12 |
13 |   ||| Analogous to `showPrec`
14 |   dshowPrec : Prec -> f a -> String
15 |   dshowPrec _ x = dshow {f} x
16 |
17 | ||| `Prelude.Show.showArg` in terms of `DShow`
18 | export
19 | dshowArg : (impl : DShow f) => f x -> String
20 | dshowArg x = " " ++ dshowPrec App x @{impl}
21 |