Théo Winterhalter (Mar 23 2022 at 16:01): Théo Winterhalter (Mar 23 2022 at 16:01):Hi! Is there any known way for going back from extracted Coq to Coq? Like I have a datatype T representing an AST in Coq which I extract in ocaml to perform some operation on it. Then I would like to get the output back in Coq as a valid .v file producing a value of the original T type.
Karl Palmskog (Mar 23 2022 at 16:05):@Théo Winterhalter have you tried Coq-of-OCaml? That's the closest tool I know of: https://github.com/formal-land/coq-of-ocaml
Maybe QuickChick has some way to track the provenance of code it extracts for running tests (https://github.com/QuickChick/QuickChick/)
Théo Winterhalter (Mar 23 2022 at 16:18):I haven't tried it, but from what I can tell it would produce a new copy of T?
Last updated: Oct 03 2023 at 20:01 UTC