padCharacter : Char- 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- Visibility: public export
horizontal : Tree -> Char- Visibility: public export
.branchMid : Tree -> Char- Visibility: public export
branchMid : Tree -> Char- Visibility: public export
.branchLast : Tree -> Char- Visibility: public export
branchLast : Tree -> Char- Visibility: public export
.vertical : Tree -> Char- Visibility: public export
vertical : Tree -> Char- Visibility: public export
.gap : Tree -> Char- Visibility: public export
gap : Tree -> Char- Visibility: public export
.placeholder : Tree -> Char- Visibility: public export
placeholder : Tree -> Char- 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- Visibility: public export
topLeft : Box -> Char- Visibility: public export
.topRight : Box -> Char- Visibility: public export
topRight : Box -> Char- Visibility: public export
.bottomLeft : Box -> Char- Visibility: public export
bottomLeft : Box -> Char- Visibility: public export
.bottomRight : Box -> Char- Visibility: public export
bottomRight : Box -> Char- Visibility: public export
.horizontal : Box -> Char- Visibility: public export
horizontal : Box -> Char- Visibility: public export
.vertical : Box -> Char- Visibility: public export
vertical : Box -> Char- 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- Visibility: public export
left : ListSyntax -> Char- Visibility: public export
.right : ListSyntax -> Char- Visibility: public export
right : ListSyntax -> Char- Visibility: public export
.separator : ListSyntax -> Char- Visibility: public export
separator : ListSyntax -> Char- 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- Visibility: public export
left : PairSyntax -> Char- Visibility: public export
.right : PairSyntax -> Char- Visibility: public export
right : PairSyntax -> Char- Visibility: public export
.separator : PairSyntax -> Char- Visibility: public export
separator : PairSyntax -> Char- Visibility: public export
SingleLineTree : Tree- Visibility: public export
DoubleLineBox : Box Double-line, to separate from tree lines
Visibility: public exportAsciiListSyntax : ListSyntax- Visibility: public export
AsciiPairSyntax : PairSyntax- Visibility: public export