TyRE.DisjointMatches

Definitions

data DisjointMatchesSnoc : Type -> Type

  A data structure to represent succesful (disjoint) matches in a string.
  A string is written here as alternatating sequence of substring and matches.
  E.g. the string "aaadeebbjk" matched against r "((a*d)|(bb))!" is represented as
  Snoc (Snoc (Prefix []) (Just 3) ['e', 'e']) Nothing ['j','k']
  Similar: DisjointMatches

Totality: total
Visibility: public export
Constructors:

Prefix : SnocList Char -> DisjointMatchesSnoc a

Snoc : DisjointMatchesSnoc a -> a -> SnocList Char -> DisjointMatchesSnoc a

Hints:

Cast (DisjointMatchesSnoc a) (DisjointMatches a)

Cast (DisjointMatches a) (DisjointMatchesSnoc a)

Functor DisjointMatchesSnoc

Show a => Show (DisjointMatchesSnoc a)

(:<) : DisjointMatchesSnoc a -> Char -> DisjointMatchesSnoc a

Visibility: export
Fixity Declarations:
infix operator, level 7
infixl operator, level 7

(:+:) : DisjointMatchesSnoc a -> a -> DisjointMatchesSnoc a

Visibility: export
Fixity Declaration: infix operator, level 6

data DisjointMatches : Type -> Type

  A data structure to represent succesful (disjoint) matches in a string.
  A string is written here as alternatating sequence of substring and matches.
  E.g. the string "aaadeebbjk" matched against r "((a*d)|(bb))!" is represented as
  Cons [] (Just 3) (Cons ['e', 'e'] Nothing (Suffix ['j','k']))
  Similar: DisjointMatchesSnoc

Totality: total
Visibility: public export
Constructors:

Suffix : List Char -> DisjointMatches a

Cons : List Char -> a -> DisjointMatches a -> DisjointMatches a

Hints:

Cast (DisjointMatchesSnoc a) (DisjointMatches a)

Cast (DisjointMatches a) (DisjointMatchesSnoc a)

Functor DisjointMatches

Show a => Show (DisjointMatches a)

(::) : DisjointMatches a -> Char -> DisjointMatches a

Visibility: export
Fixity Declarations:
infix operator, level 7
infixr operator, level 7

(.+.) : a -> DisjointMatches a -> DisjointMatches a

Visibility: export
Fixity Declaration: infix operator, level 6

(<>>) : DisjointMatchesSnoc a -> DisjointMatches a -> DisjointMatches a

Visibility: export
Fixity Declaration: infixr operator, level 6

(<><) : DisjointMatchesSnoc a -> DisjointMatches a -> DisjointMatchesSnoc a

Visibility: export
Fixity Declaration: infixl operator, level 7

toString : (a -> String) -> DisjointMatches a -> String

Visibility: export

toStringSnoc : (a -> String) -> DisjointMatchesSnoc a -> String

Visibility: export

length : DisjointMatches a -> Nat

Visibility: export