Unfortunately there is nothing to help with this currently. Robby
On Tuesday, May 10, 2016, Beta Ziliani <[email protected]> wrote: > Dear list, > > A colleague of mine used PLT Redex to define a language and its semantics, > but now he wants to prove some properties of it in Coq. He's wondering if > there is a tool to translate PLT Redex definitions into Coq ones, or if he > should write all of them from scratch. > > Many thanks, > Beta > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected] <javascript:;>. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
