Idris2Doc : Text.Token

Text.Token

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

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

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

  Projections:
  
.kind : Token k -> k
  
.text : Token k -> String
interface TokenKind : 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 -> TokType kind
  Convert a recognised string into a value. The type is determined
  by the kind of token.

Implementations:
  
TokenKind PathTokenKind
  
TokenKind JSONStringTokenKind
  
TokenKind JSONTokenKind
tokValue : TokenKind k => (kind : k) -> String -> TokType kind
  Convert a recognised string into a value. The type is determined
  by the kind of token.

  Totality: total
value : {auto conArg : TokenKind k} -> (t : Token k) -> TokType (kind t)
  Get the value of a `Token k`. The resulting type depends upon
  the kind of token.

  Totality: total