Good library or framework for handling extraction, IO, etc?

Note sure if my intent makes sense, but let’s say I have an app I want to write largely with coq, using the extraction method to run it. For at least basic, common data types that one might need, is there a library in Coq that just says “use these and your extraction will be fine,” along with utilities to do common stuff like read a file then put the data into a format that is useful to reason about in Coq etc. The goal being that the effort having to define custom extraction stuff can be saved for novel types.

Is this something that exists? If not, is it just because this part of extraction isn’t as annoying as it appears? Appreciate tips!

1 Like

I’m a heavy user of Coq extraction, and find this IO library convenient in most cases:


Interesting. How does that relate to:
Which has similar goals?

AFAIK coq-simple-io is simpler than coq-io as its name suggests, and provides an IO monad that is similar to Haskell.