TyRE.RE

Definitions

data RE : Type

Totality: total
Visibility: public export
Constructors:

Exactly : Char -> RE

OneOf : List Char -> RE

To : Char -> Char -> RE

Any : RE

Concat : RE -> RE -> RE

Alt : RE -> RE -> RE

Maybe : RE -> RE

Group : RE -> RE

Rep0 : RE -> RE

Rep1 : RE -> RE

Keep : RE -> RE

Hints:

Eq RE

Show RE

specialChars : String

Visibility: public export

mapChar : Char -> String

Visibility: public export

isUnit : RE -> Bool

Visibility: public export

isSemiUnit : RE -> Bool

Visibility: public export

pshow : (RE -> Bool) -> RE -> String

  If condintion is satisfied show in parentheses

Visibility: public export

showAux : RE -> String

Visibility: public export

CodeShapeREKeep : RE -> Code

Visibility: public export

CodeShapeRE : RE -> Code

Visibility: public export

TypeREKeep : RE -> Type

Visibility: public export

TypeRE : RE -> Type

Visibility: public export

pairEq : (a, x) = (b, y) -> (a = b, x = y)

Visibility: export

eitherToMaybeL : Either a () -> Maybe a

Visibility: export

eitherToMaybeR : Either () a -> Maybe a

Visibility: export

altTyREKeep : (re1 : RE) -> (re2 : RE) -> SimplifyCode (CodeShapeREKeep re1) = a -> SimplifyCode (CodeShapeREKeep re2) = b -> TyRE (Either (Sem a) (Sem b))

Visibility: public export

concatTyREKeep : (re1 : RE) -> (re2 : RE) -> TyRE (TypeREKeep re1, TypeREKeep re2)

Visibility: public export

compileKeep : (re : RE) -> TyRE (TypeREKeep re)

Visibility: public export

altTyRE : (re1 : RE) -> (re2 : RE) -> SimplifyCode (CodeShapeRE re1) = a -> SimplifyCode (CodeShapeRE re2) = b -> TyRE (Either (Sem a) (Sem b))

Visibility: public export

concatTyRE : (re1 : RE) -> (re2 : RE) -> TyRE (TypeRE re1, TypeRE re2)

Visibility: public export

compile : (re : RE) -> TyRE (TypeRE re)

Visibility: public export