Idris2Doc : Language.JSON.Tokens

Language.JSON.Tokens

Definitions

strTrue : String
Totality: total
Visibility: public export
strFalse : String
Totality: total
Visibility: public export
data Bracket : Type
Totality: total
Visibility: public export
Constructors:
Open : Bracket
Close : Bracket

Hint: 
Eq Bracket
data Punctuation : Type
Totality: total
Visibility: public export
Constructors:
Comma : Punctuation
Colon : Punctuation
Square : Bracket -> Punctuation
Curly : Bracket -> Punctuation

Hint: 
Eq Punctuation
data JSONTokenKind : Type
Totality: total
Visibility: public export
Constructors:
JTBoolean : JSONTokenKind
JTNumber : JSONTokenKind
JTString : JSONTokenKind
JTNull : JSONTokenKind
JTPunct : Punctuation -> JSONTokenKind
JTIgnore : JSONTokenKind

Hints:
Eq JSONTokenKind
TokenKind JSONTokenKind
JSONToken : Type
Totality: total
Visibility: public export
ignored : WithBounds JSONToken -> Bool
Totality: total
Visibility: export