Stream: Coq users

Topic: Integer parsing and printing


view this post on Zulip Armaël Guéneau (Aug 17 2020 at 10:05):

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.

view this post on Zulip Karl Palmskog (Aug 17 2020 at 10:09):

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)

view this post on Zulip Armaël Guéneau (Aug 17 2020 at 10:13):

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

view this post on Zulip Karl Palmskog (Aug 17 2020 at 10:17):

it is/was used in the oeuf project: https://github.com/uwplse/oeuf http://oeuf.uwplse.org

view this post on Zulip Karl Palmskog (Aug 17 2020 at 10:18):

for the record, PrettyParsing builds with at least 8.7 - 8.12 if you install StructTact first: https://github.com/uwplse/StructTact

view this post on Zulip Pierre Roux (Aug 17 2020 at 10:21):

In the stdlib you have Numbers.DecimalString but this is also probably way more basic than what you need.

view this post on Zulip Armaël Guéneau (Aug 17 2020 at 10:27):

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)

view this post on Zulip Armaël Guéneau (Aug 17 2020 at 10:28):

ah wait no, I'm getting confused

view this post on Zulip Armaël Guéneau (Aug 17 2020 at 10:36):

(looks like all the good stuff is available in 8.9 as well)


Last updated: Feb 08 2023 at 23:03 UTC