TyRE.Text.Token

This is a slightly modified copy of the same module from `contrib` package.

Definitions

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.

TokType : TokenKind k => k -> Type

  The type that a token of this kind converts to.

Visibility: public export

tokValue : {auto __con : TokenKind k} -> (kind : k) -> String -> TokType kind

  Convert a recognised string into a value. The type is determined
  by the kind of token.

Visibility: public export

record Token : Type -> Type

  A token of a particular kind and the text that was recognised.

Totality: total
Visibility: public export
Constructor: 

Tok : k -> String -> Token k

Projections:

.kind : Token k -> k

.text : Token k -> String

.kind : Token k -> k

Visibility: public export

kind : Token k -> k

Visibility: public export

.text : Token k -> String

Visibility: public export

text : Token k -> String

Visibility: public export

value : {auto {conArg:956} : TokenKind k} -> (t : Token k) -> TokType (kind t)

  Get the value of a `Token k`. The resulting type depends upon
  the kind of token.

Visibility: public export