Idris2Doc : Text.Regex.Parser.ERE

Text.Regex.Parser.ERE

Parser of extended POSIX regular expressions with (hopefully) unambiguous extensions from PCRE.

Reexports

import public Data.Either
import public Data.DPair
import public Language.Reflection
import public Text.Regex.Interface
import public Text.Regex.Parser

Definitions

postfixOp : Regex rx => PostfixOp -> rx a -> Exists rx

Totality: total
Visibility: public export

crumple : Monoid a => List (n : Nat ** f (Vect n a)) -> Exists (\tys => (All f tys, (n : Nat ** (All id tys -> Vect n a, Any id tys -> Vect n a))))

Totality: total
Visibility: public export

parseRegex : Regex rx => String -> Either BadRegex (n : Nat ** rx (Vect n String))

Totality: total
Visibility: export

parseRegexN : Regex rx => (matchingGroupsCnt : Nat) -> String -> Either BadRegex (rx (Vect matchingGroupsCnt String))

Totality: total
Visibility: export

parseAnyRegex : Regex rx => String -> Either BadRegex (Exists rx)

  Parses regex with any returning type and retuns both the type and parsed regex

Totality: total
Visibility: export

toRegex : {auto {conArg:5580} : Regex rx} -> (s : String) -> {auto 0 {conArg:5586} : IsRight (parseRegex s)} -> rx (Vect (fst (fromRight (parseRegex s))) String)

Totality: total
Visibility: public export

.erx : Regex rx => String -> Elab (rx a)

Totality: total
Visibility: export