TyRE

Reexports

Definitions

data TyRE : Type -> Type

Totality: total
Visibility: public export
Constructors:

Untyped : (r : CoreRE) -> TyRE (Shape r)

(<*>) : 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 (List a)

Hint: 

Functor TyRE

compile : TyRE a -> CoreRE

Visibility: export

extract : (tyre : TyRE a) -> Shape (compile tyre) -> a

Visibility: export

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

Visibility: export

empty : TyRE ()

Visibility: export

any : TyRE Char

Visibility: export

group : TyRE a -> TyRE String

Visibility: export

ignore : TyRE a -> TyRE ()

Visibility: export

range : Char -> Char -> TyRE Char

Visibility: export

digit : TyRE Integer

Visibility: export

digitChar : TyRE Char

Visibility: export

oneOfList : List Char -> TyRE Char

Visibility: export

oneOf : String -> TyRE Char

Visibility: export

match : Char -> TyRE ()

Visibility: export

rep0 : TyRE a -> TyRE (List a)

Visibility: export

rep1 : TyRE a -> TyRE (List a)

Visibility: export

option : TyRE a -> TyRE (Maybe a)

Visibility: export

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

Visibility: export
Fixity Declaration: infixl operator, level 3

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

Visibility: export
Fixity Declaration: infixl operator, level 3

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

Visibility: export

letter : TyRE Char

Visibility: export

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

Visibility: export

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

Visibility: export

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

Visibility: export

repTimesType : Nat -> Type -> Type

Visibility: public export

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

Visibility: export