CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation
12 stars 3 forks source link

Support for `Fixpoint` in the translation #4

Open herbelin opened 3 years ago

herbelin commented 3 years ago

Hi, I realized that Forcing Translate foo is not implemented for fix?

In principle, it should be possible to it by hand using Forcing Definition but I wonder what would be the difficulties to do it automatically?