Return bounded nats for `decimalDigit`

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

Return bounded nats for `decimalDigit` #38

Closed gallais closed 4 years ago

gallais commented 4 years ago

At the moment decimalDigit in TParsec.Combinators.Numbers returns a Nat when it should return a Nat together with the proof it is less than 10. I don't think it's worth using Fin here as we do want natural numbers in the other parsers using decimalDigit.

gallais commented 4 years ago

Fixed by 75b288719b9781273a595c294b7d3bed5ea1904d