TyRE.Core

Reexports

Definitions

data CharCond : Type

Totality: total
Visibility: public export
Constructors:

OneOf : SortedSet Char -> CharCond

Range : (Char, Char) -> CharCond

Pred : (Char -> Bool) -> CharCond

Hint: 

Eq CharCond

satisfies : CharCond -> Char -> Bool

Visibility: public export

data TyRE : Type -> Type

Totality: total
Visibility: public export
Constructors:

Empty : TyRE ()

MatchChar : CharCond -> TyRE Char

Group : TyRE a -> TyRE String

(<*>) : TyRE a -> TyRE b -> TyRE (a, b)

Conv : TyRE a -> (a -> b) -> TyRE b

(<|>) : TyRE a -> TyRE b -> TyRE (Either a b)

Rep : TyRE a -> TyRE (SnocList a)

Hint: 

Functor TyRE

predicate : (Char -> Bool) -> TyRE Char

Visibility: public export

empty : TyRE ()

Visibility: public export

any : TyRE Char

Visibility: public export

group : TyRE a -> TyRE String

Visibility: public export

ignore : TyRE a -> TyRE ()

Visibility: public export

range : Char -> Char -> TyRE Char

Visibility: public export

digit : TyRE Integer

Visibility: public export

digitChar : TyRE Char

Visibility: public export

oneOfCharsList : List Char -> TyRE Char

Visibility: public export

oneOfChars : String -> TyRE Char

Visibility: public export

match : Char -> TyRE ()

Visibility: public export

rep0 : TyRE a -> TyRE (List a)

Visibility: public export

rep1 : TyRE a -> TyRE (List a)

Visibility: public export

rep1l1 : TyRE a -> TyRE (List1 a)

Visibility: public export

option : TyRE a -> TyRE (Maybe a)

Visibility: public export

(*>) : TyRE a -> TyRE b -> TyRE b

Visibility: public export
Fixity Declarations:
infixl operator, level 3
infixr operator, level 6

(<*) : TyRE a -> TyRE b -> TyRE a

Visibility: public export
Fixity Declarations:
infixl operator, level 3
infixr operator, level 6

or : TyRE a -> TyRE a -> TyRE a

Visibility: public export

oneOf : List1 (TyRE a) -> TyRE a

Visibility: public export

letter : TyRE Char

Visibility: public export

repFrom : Nat -> TyRE a -> TyRE (List a)

Visibility: public export

repTo : Nat -> TyRE a -> TyRE (List a)

Visibility: public export

repFromTo : (from : Nat) -> (to : Nat) -> from <= to = True => TyRE a -> TyRE (List a)

Visibility: public export

repTimesType : Nat -> Type -> Type

Visibility: public export

repTimes : (n : Nat) -> TyRE a -> TyRE (repTimesType n a)

Visibility: public export

isConsuming : TyRE a -> Bool

Visibility: public export

data IsConsuming : TyRE a -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsConsuming : {auto 0 _ : isConsuming re = True} -> IsConsuming re