padCharacter : Char- Totality: total
Visibility: public export record Tree : Type- Totality: total
Visibility: public export
Constructor: MkTree : Char -> Char -> Char -> Char -> Char -> Char -> Tree
Projections:
.branchLast : Tree -> Char.branchMid : Tree -> Char.gap : Tree -> Char.horizontal : Tree -> Char.placeholder : Tree -> Char.vertical : Tree -> Char
.horizontal : Tree -> Char- Totality: total
Visibility: public export horizontal : Tree -> Char- Totality: total
Visibility: public export .branchMid : Tree -> Char- Totality: total
Visibility: public export branchMid : Tree -> Char- Totality: total
Visibility: public export .branchLast : Tree -> Char- Totality: total
Visibility: public export branchLast : Tree -> Char- Totality: total
Visibility: public export .vertical : Tree -> Char- Totality: total
Visibility: public export vertical : Tree -> Char- Totality: total
Visibility: public export .gap : Tree -> Char- Totality: total
Visibility: public export gap : Tree -> Char- Totality: total
Visibility: public export .placeholder : Tree -> Char- Totality: total
Visibility: public export placeholder : Tree -> Char- Totality: total
Visibility: public export record Box : Type Used for drawing a box border
Totality: total
Visibility: public export
Constructor: MkBox : Char -> Char -> Char -> Char -> Char -> Char -> Box
Projections:
.bottomLeft : Box -> Char.bottomRight : Box -> Char.horizontal : Box -> Char.topLeft : Box -> Char.topRight : Box -> Char.vertical : Box -> Char
.topLeft : Box -> Char- Totality: total
Visibility: public export topLeft : Box -> Char- Totality: total
Visibility: public export .topRight : Box -> Char- Totality: total
Visibility: public export topRight : Box -> Char- Totality: total
Visibility: public export .bottomLeft : Box -> Char- Totality: total
Visibility: public export bottomLeft : Box -> Char- Totality: total
Visibility: public export .bottomRight : Box -> Char- Totality: total
Visibility: public export bottomRight : Box -> Char- Totality: total
Visibility: public export .horizontal : Box -> Char- Totality: total
Visibility: public export horizontal : Box -> Char- Totality: total
Visibility: public export .vertical : Box -> Char- Totality: total
Visibility: public export vertical : Box -> Char- Totality: total
Visibility: public export record ListSyntax : Type Used for rendering list-like syntax
Totality: total
Visibility: public export
Constructor: MkListSyntax : Char -> Char -> Char -> ListSyntax
Projections:
.left : ListSyntax -> Char.right : ListSyntax -> Char.separator : ListSyntax -> Char
.left : ListSyntax -> Char- Totality: total
Visibility: public export left : ListSyntax -> Char- Totality: total
Visibility: public export .right : ListSyntax -> Char- Totality: total
Visibility: public export right : ListSyntax -> Char- Totality: total
Visibility: public export .separator : ListSyntax -> Char- Totality: total
Visibility: public export separator : ListSyntax -> Char- Totality: total
Visibility: public export record PairSyntax : Type Used for rendering pair-like syntax
Totality: total
Visibility: public export
Constructor: MkPairSyntax : Char -> Char -> Char -> PairSyntax
Projections:
.left : PairSyntax -> Char.right : PairSyntax -> Char.separator : PairSyntax -> Char
.left : PairSyntax -> Char- Totality: total
Visibility: public export left : PairSyntax -> Char- Totality: total
Visibility: public export .right : PairSyntax -> Char- Totality: total
Visibility: public export right : PairSyntax -> Char- Totality: total
Visibility: public export .separator : PairSyntax -> Char- Totality: total
Visibility: public export separator : PairSyntax -> Char- Totality: total
Visibility: public export SingleLineTree : Tree- Totality: total
Visibility: public export DoubleLineBox : Box Double-line, to separate from tree lines
Totality: total
Visibility: public exportAsciiListSyntax : ListSyntax- Totality: total
Visibility: public export AsciiPairSyntax : PairSyntax- Totality: total
Visibility: public export