Does the fact that the guard checker for Template is axiomatized mean that it's not actually possible to build closed typing derivations of (co)fixpoints?
I think you're right.
If I remember correctly, Nicolas had to instantiate the checker with a dummy, constant-true function when trying to test the checker
Yes, you're right
Jason Gross has marked this topic as resolved.
Last updated: Jun 01 2023 at 12:01 UTC