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
Last updated: Jan 30 2023 at 19:04 UTC