Stream: Coq users

Topic: Reverse extraction?

view this post on Zulip Philipp G. Haselwarter (Nov 18 2021 at 16:56):

I have a Coq file Expr.v that gets extracted to, and I have a compiler front end that produces values for the types in Is there a way to "un-extract" and pretty-print these OCaml values to the datatypes defined in Expr.v?

view this post on Zulip Karl Palmskog (Nov 18 2021 at 16:58):

the closest you have in this direction is probably CoqOfOCaml, but extraction changes names a lot, so would be surprised to see a full reconnection.

Last updated: Jun 25 2024 at 15:02 UTC