Idris2Doc : Text.Regex.Naive

Text.Regex.Naive

(source)
Reexports
import public Data.Alternative
import public Data.List.Quantifiers
import public Data.List.Lazy
import public Data.List1
import public Data.Vect
import public Syntax.IHateParens.List
import public Text.Regex.Interface
import public Text.Matcher
Definitions
data RegExpOp : Type -> Type
  Totality: total
  Visibility: export
  Constructors:
  
Seq : All RegExp tys -> RegExpOp (All id tys)
  
Sel : All RegExp tys -> RegExpOp (Any id tys)
  
WordB : Bool -> Bool -> RegExpOp ()
  
WithMatch : RegExp a -> RegExpOp (List Char, a)
  
Rep1 : RegExp a -> RegExpOp (List1 a)
  
Edge : LineMode -> EdgeSide -> RegExpOp ()
  
AnyChar : LineMode -> RegExpOp Char
  
Sym : (Char -> Maybe a) -> RegExpOp a
record RegExp : Type -> Type
  Totality: total
  Visibility: export
  Constructor: 
RE : RegExpOp opTy -> (opTy -> a) -> RegExp a

  Projections:
  
.mapping : ({rec:0} : RegExp a) -> opTy {rec:0} -> a
  
0 .opTy : RegExp a -> Type
  
.operation : ({rec:0} : RegExp a) -> RegExpOp (opTy {rec:0})

  Hints:
  
Alternative RegExp
  
Applicative RegExp
  
Functor RegExp
  
Regex RegExp
  
TextMatcher RegExp
rawMatch : Bool -> RegExp a -> List Char -> (str : List Char) -> LazyList (Maybe (Fin (S (str .length))), a)
  Totality: total
  Visibility: public export
rawMatchIn : Bool -> RegExp a -> List Char -> List Char -> LazyList (List Char, (List Char, (a, List Char)))
  Totality: total
  Visibility: public export
rawMatchAll : Bool -> RegExp a -> List Char -> List Char -> LazyList (List (List Char, (List Char, a)), List Char)
  Totality: total
  Visibility: public export
RegexRegExp : Regex RegExp
  Totality: total
  Visibility: public export
TextMatcherRegExp : TextMatcher RegExp
  Totality: total
  Visibility: public export