Is DecEq necessary for tokens?
clayrat opened this issue · 1 comments
clayrat commented
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
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.