interface Pretty : Type -> Type- Parameters: a
Constructor: MkPretty
Methods:
prettyPrec : Prec -> a -> Doc opts
Implementations:
Pretty Char Pretty String Pretty Bits8 Pretty Bits16 Pretty Bits32 Pretty Bits64 Pretty Int8 Pretty Int16 Pretty Int32 Pretty Int64 Pretty Integer Pretty Double Pretty () Pretty Bool Pretty Ordering Pretty Nat Pretty Int Pretty a => Pretty (Maybe a) Pretty a => Pretty b => Pretty (Either a b) Pretty a => Pretty (List a) Pretty a => Pretty (List1 a) Pretty a => Pretty (SnocList a) Pretty a => Pretty b => Pretty (a, b) Pretty a => Pretty (Vect n a) Pretty k => Pretty v => Pretty (SortedMap k v) Pretty k => Pretty (SortedSet k)
prettyPrec : Pretty a => Prec -> a -> Doc opts- Totality: total
Visibility: public export pretty : Pretty a => a -> Doc opts Alias for `prettyPrec Open`
Totality: total
Visibility: public exportprettyArg : Pretty a => a -> Doc opts Alias for `prettyPrec App`
Totality: total
Visibility: public exportprettyCon : Prec -> String -> List (Doc opts) -> Doc opts Utility for pretty printing Idris data types.
Constructor name and arguments are layed out on a single line
if and only if they fit the page width
and all pretty printed arguments use only a single line. If
one of these conditions does not hold, the list of arguments is
indented by two spaces and layed out vertically after the constructor
name.
```idris example
prettyCon "Just" [prettyArg v]
```
Totality: total
Visibility: exportprettyField : Pretty a => String -> a -> Doc opts Utility for pretty printing Idris record fields.
Field name and value are separated by an equals sign (`=`) and
layed out on a single line if and only if they fit the page width
and the pretty printed values is itself on a single line. If
one of these conditions does not hold, the value is placed on
the next line and indented by two spaces.
Totality: total
Visibility: exportprettyRecord : Prec -> String -> List (Doc opts) -> Doc opts Utility for pretty printing Idris data types with named arguments.
This uses record syntax for printing the argument list, but is not
limited to single-constructor data types.
Constructor name and arguments are layed out on a single line
if and only if they fit the page width
and all pretty printed arguments use only a single line. If
one of these conditions does not hold, the list of arguments is
indented by two spaces and layed out vertically after the constructor
name.
```idris example
prettyCon "Just" [prettyArg v]
```
Note: Use `prettyField` to pair an argument with its field name.
Totality: total
Visibility: exportThroughPretty : Pretty a => LayoutOpts => Interpolation a- Totality: total
Visibility: export