Add conversion functions to structural desc of disjoint matches #46
Conversation
| disjointMatches : (re : TyRE a) -> {auto 0 consuming : IsConsuming re} | ||
| -> List Char -> (greedy : Bool) | ||
| -> (List (List Char, a), List Char) |
There was a problem hiding this comment.
The API for our lib is in Data.Regex, so if you want to have this outside of this lib it should most probably be there. I think it's reasonable to drop the current asDisjointMatches from there.
There was a problem hiding this comment.
I started by thinking it should be dropped, but then I thought it does express the inductive pattern better, so maybe it's useful to export it. What do you think?
There was a problem hiding this comment.
Well, I see a benefit in using common data structures instead of ones defined in TyRE. It feels potentially more flexible and easier to understand for the end user. On the other hand, the type looks a bit less pleasant. Otherwise, I don't see much of a difference. I'd decide only for one of those to be exported, but I'm not sure which one it should be.
No description provided.