Idris2Doc : Text.Matcher

Text.Matcher

(source)
Reexports
import public Data.Maybe
Definitions
record OneMatchInside : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkOneMatchInside : String -> String -> a -> String -> OneMatchInside a

  Projections:
  
.matchedStr : OneMatchInside a -> String
  
.matchedVal : OneMatchInside a -> a
  
.unmatchedPost : OneMatchInside a -> String
  
.unmatchedPre : OneMatchInside a -> String
.unmatchedPre : OneMatchInside a -> String
  Totality: total
  Visibility: public export
unmatchedPre : OneMatchInside a -> String
  Totality: total
  Visibility: public export
.matchedStr : OneMatchInside a -> String
  Totality: total
  Visibility: public export
matchedStr : OneMatchInside a -> String
  Totality: total
  Visibility: public export
.matchedVal : OneMatchInside a -> a
  Totality: total
  Visibility: public export
matchedVal : OneMatchInside a -> a
  Totality: total
  Visibility: public export
.unmatchedPost : OneMatchInside a -> String
  Totality: total
  Visibility: public export
unmatchedPost : OneMatchInside a -> String
  Totality: total
  Visibility: public export
forgetVal : OneMatchInside a -> (String, (String, String))
  Totality: total
  Visibility: public export
data AllMatchedInside : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Stop : String -> AllMatchedInside a
  
Match : String -> String -> a -> AllMatchedInside a -> AllMatchedInside a
matchedCnt : AllMatchedInside a -> Nat
  Totality: total
  Visibility: public export
matchedStrs' : (ms : AllMatchedInside a) -> Vect (matchedCnt ms) String
  Totality: total
  Visibility: public export
matchedVals' : (ms : AllMatchedInside a) -> Vect (matchedCnt ms) a
  Totality: total
  Visibility: public export
matchedStrs : AllMatchedInside a -> List String
  Totality: total
  Visibility: public export
matchedVals : AllMatchedInside a -> List a
  Totality: total
  Visibility: public export
interface TextMatcher : (Type -> Type) -> Type
  Parameters: tm
Methods:
  
matchWhole' : Bool -> tm a -> String -> Maybe a
  
matchInside' : Bool -> tm a -> String -> Maybe (OneMatchInside a)
  
matchAll' : Bool -> tm a -> String -> AllMatchedInside a
matchWhole' : TextMatcher tm => Bool -> tm a -> String -> Maybe a
  Totality: total
  Visibility: public export
matchInside' : TextMatcher tm => Bool -> tm a -> String -> Maybe (OneMatchInside a)
  Totality: total
  Visibility: public export
matchAll' : TextMatcher tm => Bool -> tm a -> String -> AllMatchedInside a
  Totality: total
  Visibility: public export
matchWhole : {default False _ : Bool} -> TextMatcher tm => tm a -> String -> Maybe a
  Totality: total
  Visibility: public export
matchInside : {default False _ : Bool} -> TextMatcher tm => tm a -> String -> Maybe (OneMatchInside a)
  Totality: total
  Visibility: public export
matchAll : {default False _ : Bool} -> TextMatcher tm => tm a -> String -> AllMatchedInside a
  Totality: total
  Visibility: public export
MatchesWhole : {default False _ : Bool} -> TextMatcher tm => tm a -> String -> Type
  Totality: total
  Visibility: public export
MatchesInside : {default False _ : Bool} -> TextMatcher tm => tm a -> String -> Type
  Totality: total
  Visibility: public export
doesMatchWhole : {default False multiline : Bool} -> {auto {conArg:1667} : TextMatcher tm} -> (matcher : tm a) -> (input : String) -> Dec MatchesWhole
  Totality: total
  Visibility: public export
doesMatchInside : {default False multiline : Bool} -> {auto {conArg:1667} : TextMatcher tm} -> (matcher : tm a) -> (input : String) -> Dec MatchesInside
  Totality: total
  Visibility: public export
matchWholeResult : {default False multiline : Bool} -> {auto {conArg:1667} : TextMatcher tm} -> (matcher : tm a) -> (input : String) -> {auto 0 _ : MatchesWhole} -> a
  Totality: total
  Visibility: public export
matchInsideResult : {default False multiline : Bool} -> {auto {conArg:1667} : TextMatcher tm} -> (matcher : tm a) -> (input : String) -> {auto 0 _ : MatchesInside} -> OneMatchInside a
  Totality: total
  Visibility: public export
replaceOne : {default False _ : Bool} -> TextMatcher tm => tm a -> (String -> a -> String) -> String -> String
  Totality: total
  Visibility: export
replaceAll : {default False _ : Bool} -> TextMatcher tm => tm a -> (String -> a -> String) -> String -> String
  Totality: total
  Visibility: export
.str : (t -> (String -> a -> String) -> String -> String) -> t -> (String -> String) -> String -> String
  Totality: total
  Visibility: public export
.val : (t -> (String -> a -> String) -> String -> String) -> t -> (a -> String) -> String -> String
  Totality: total
  Visibility: public export
.const : (t -> (String -> a -> String) -> String -> String) -> t -> String -> String -> String
  Totality: total
  Visibility: public export