Jason Gross (Nov 02 2022 at 18:59): Jason Gross (Nov 02 2022 at 18:59):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?
Théo Winterhalter (Nov 02 2022 at 19:38):I think you're right.
Meven Lennon-Bertrand (Nov 07 2022 at 14:18):If I remember correctly, Nicolas had to instantiate the checker with a dummy, constant-true function when trying to test the checker
Matthieu Sozeau (Nov 23 2022 at 12:51):Yes, you're right
Notification Bot (Nov 23 2022 at 13:10):Jason Gross has marked this topic as resolved.
Last updated: Jun 01 2023 at 12:01 UTC