Protocol.IDE.Formatting

Definitions

data Formatting : Type

Totality: total
Visibility: public export
Constructors:

Bold : Formatting

Italic : Formatting

Underline : Formatting

Hints:

FromSExpable Formatting

SExpable Formatting

Show Formatting

record Properties : Type

Totality: total
Visibility: public export
Constructor: 

MkProperties : Maybe Decoration -> Maybe Formatting -> Properties

Projections:

.decor : Properties -> Maybe Decoration

.format : Properties -> Maybe Formatting

Hints:

FromSExpable Properties

SExpable Properties

.decor : Properties -> Maybe Decoration

Totality: total
Visibility: public export

decor : Properties -> Maybe Decoration

Totality: total
Visibility: public export

.format : Properties -> Maybe Formatting

Totality: total
Visibility: public export

format : Properties -> Maybe Formatting

Totality: total
Visibility: public export

mkDecor : Decoration -> Properties

Totality: total
Visibility: export

mkFormat : Formatting -> Properties

Totality: total
Visibility: export