Idris2Doc : Text.Token

Text.Token

TokType : TokenKindk => k -> Type
  The type that a token of this kind converts to.

Totality: total
recordToken : Type -> Type
  A token of a particular kind and the text that was recognised.

Totality: total
Constructor: 
Tok : k -> String -> Tokenk

Projections:
.kind : Tokenk -> k
.text : Tokenk -> String
interfaceTokenKind : Type -> Type
  For a type `kind`, specify a way of converting the recognised
string into a value.

```idris example
data SimpleKind = SKString | SKInt | SKComma

TokenKind SimpleKind where
TokType SKString = String
TokType SKInt = Int
TokType SKComma = ()

tokValue SKString x = x
tokValue SKInt x = cast x
tokValue SKComma x = ()
```

Parameters: k
Methods:
TokType : k -> Type
  The type that a token of this kind converts to.
tokValue : (kind : k) -> String -> TokTypekind
  Convert a recognised string into a value. The type is determined
by the kind of token.

Implementations:
TokenKindPathTokenKind
TokenKindJSONStringTokenKind
TokenKindJSONTokenKind
tokValue : TokenKindk => (kind : k) -> String -> TokTypekind
  Convert a recognised string into a value. The type is determined
by the kind of token.

Totality: total
value : {autoconArg : TokenKindk} -> (t : Tokenk) -> TokType (kindt)
  Get the value of a `Token k`. The resulting type depends upon
the kind of token.

Totality: total