Is anyone aware of Coq code (and associated lemmas) for parsing (and printing) nats from strings? I found https://github.com/arthuraa/poleiro/blob/master/theories/ReadNat.v which is a good start but doesn't have all the lemmas that I would like to, so I'm wondering if there's a more complete formalization somewhere.
this may be able to do what you're looking for: https://github.com/wilcoxjay/PrettyParsing (see, e.g., https://github.com/wilcoxjay/PrettyParsing/blob/master/Example.v)
Thanks! And it seems we have similar motivations :). I'm also converting between binder representations! Now I'm curious about the context behind this PrettyParsing project
it is/was used in the oeuf project: https://github.com/uwplse/oeuf http://oeuf.uwplse.org
for the record, PrettyParsing builds with at least 8.7 - 8.12 if you install StructTact first: https://github.com/uwplse/StructTact
In the stdlib you have
Numbers.DecimalString but this is also probably way more basic than what you need.
Oh, I didn't know about that module! It might be enough for my needs actually, provided I switch to a more recent Coq version (I'm using 8.9 currently, and the module doesn't contain much there)
ah wait no, I'm getting confused
(looks like all the good stuff is available in 8.9 as well)
Last updated: Dec 01 2023 at 06:01 UTC