Idris2Doc : Protocol.IDE.Formatting

Protocol.IDE.Formatting

(source)

Definitions

dataFormatting : Type
Totality: total
Visibility: public export
Constructors:
Bold : Formatting
Italic : Formatting
Underline : Formatting

Hints:
FromSExpableFormatting
SExpableFormatting
ShowFormatting
recordProperties : Type
Totality: total
Visibility: public export
Constructor: 
MkProperties : MaybeDecoration->MaybeFormatting->Properties

Projections:
.decor : Properties->MaybeDecoration
.format : Properties->MaybeFormatting

Hints:
FromSExpableProperties
SExpableProperties
.decor : Properties->MaybeDecoration
Totality: total
Visibility: public export
decor : Properties->MaybeDecoration
Totality: total
Visibility: public export
.format : Properties->MaybeFormatting
Totality: total
Visibility: public export
format : Properties->MaybeFormatting
Totality: total
Visibility: public export
mkDecor : Decoration->Properties
Totality: total
Visibility: export
mkFormat : Formatting->Properties
Totality: total
Visibility: export