diff --git a/src/TyRE/DisjointMatches.idr b/src/TyRE/DisjointMatches.idr
index eef9cbd..437dc7f 100644
--- a/src/TyRE/DisjointMatches.idr
+++ b/src/TyRE/DisjointMatches.idr
@@ -4,7 +4,6 @@ import Data.SnocList
 import Data.List
 
 infix 6 :+:,.+.
-infix 7 :<,::
 
 ||| A data structure to represent succesful (disjoint) matches in a string.
 ||| A string is written here as alternatating sequence of substring and matches.
@@ -35,10 +34,30 @@ data DisjointMatches : Type -> Type where
   Suffix : List Char -> DisjointMatches a
   Cons : List Char -> a -> DisjointMatches a -> DisjointMatches a
 
+public export
+DisjointMatchesExplicit : Type -> Type
+DisjointMatchesExplicit a = (List (List Char, a), List Char)
+
+public export
+Cast (DisjointMatches a) (DisjointMatchesExplicit a) where
+  cast (Suffix cs) = ([], cs)
+  cast (Cons cs x ps) =
+    let (dsx, cs) = cast {to = DisjointMatchesExplicit a} ps
+    in ((cs,x) :: dsx, cs)
+
+public export
+curryCast : List (List Char, a) -> List Char -> DisjointMatches a
+curryCast [] cs = Suffix cs
+curryCast ((ds, x) :: dsx) cs = Cons ds x $ curryCast dsx cs
+
+public export
+Cast (DisjointMatchesExplicit a) (DisjointMatches a) where
+  cast = uncurry curryCast
+
 export
-(::) : DisjointMatches a -> Char -> DisjointMatches a
-(::) (Suffix cs) c = Suffix (c :: cs)
-(::) (Cons cs parse tail) c = Cons (c :: cs) parse tail
+(::) : Char -> DisjointMatches a -> DisjointMatches a
+(::) c (Suffix cs) = Suffix (c :: cs)
+(::) c (Cons cs parse tail) = Cons (c :: cs) parse tail
 
 export
 (.+.) : a -> DisjointMatches a -> DisjointMatches a
diff --git a/src/TyRE/Parser.idr b/src/TyRE/Parser.idr
index 8c8b795..55fa226 100644
--- a/src/TyRE/Parser.idr
+++ b/src/TyRE/Parser.idr
@@ -38,7 +38,7 @@ asDisjointMatches re cs greedy =
         then runFromInit (runTillLastAccept cs Nothing)
         else runFromInit (runTillFirstAccept cs)
       matchesRec : List Char -> DisjointMatchesSnoc a
-                -> DisjointMatchesSnoc a 
+                -> DisjointMatchesSnoc a
       matchesRec [] dm = dm
       matchesRec (x :: xs) dm with (parseFunction (x :: xs))
         matchesRec (x :: xs) dm | (Nothing, _) = matchesRec xs (dm :< x)
@@ -46,6 +46,13 @@ asDisjointMatches re cs greedy =
           matchesRec tail (dm :+: tree)
   in cast (matchesRec cs (Prefix [<]))
 
+export
+partial --we should be able to prove totality thanks to `consuming`
+disjointMatches : (re : TyRE a) -> {auto 0 consuming : IsConsuming re}
+                  -> List Char -> (greedy : Bool)
+                  -> (List (List Char, a), List Char)
+disjointMatches re str greedy = cast $ asDisjointMatches re str greedy
+
 export
 partial
 getToken : (r : TyRE a) -> Stream Char -> (greedy : Bool)