Idris.Doc.Annotations

Definitions

data IdrisDocAnn : Type

Totality: total
Visibility: public export
Constructors:

Header : IdrisDocAnn

Deprecation : IdrisDocAnn

Declarations : IdrisDocAnn

Decl : Name -> IdrisDocAnn

DocStringBody : IdrisDocAnn

UserDocString : IdrisDocAnn

Syntax : IdrisSyntax -> IdrisDocAnn

Hint: 

Pretty IdrisDocAnn CDef

docToDecoration : IdrisDocAnn -> Maybe Decoration

Totality: total
Visibility: export

styleAnn : IdrisDocAnn -> AnsiStyle

Totality: total
Visibility: export

tCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn

Totality: total
Visibility: export

dCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn

Totality: total
Visibility: export

fun : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn

Totality: total
Visibility: export

header : Doc IdrisDocAnn -> Doc IdrisDocAnn

Totality: total
Visibility: export