search

gallais / idris-tparsec

TParsec - Total Parser Combinators in Idris
https://gallais.github.io/idris-tparsec/
GNU General Public License v3.0
93 stars 10 forks source link

Is DecEq necessary for tokens? #8

Closed clayrat closed 6 years ago

clayrat commented 6 years ago

As far I see, the DecEq constraint on tokens is only used in Combinators.exact, where it is immediately converted to a boolean. Seems like a weaker Eq constraint could be used here, sparing the user of writing things like counterproofs. Is this an artifact of an Agda port, or did you intend to have this constraint?

gallais commented 6 years ago

Is this an artifact of an Agda port, or did you intend to have this constraint?

It's more of a semantical statement about what exact is doing. I wouldn't be opposed to changing the constraint as the extra information is indeed not being used.