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!