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 expr.ml, and I have a compiler front end that produces values for the types in expr.ml. Is there a way to "un-extract" and pretty-print these expr.ml 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: Oct 03 2023 at 20:01 UTC