Stream: MetaCoq

Topic: ✔ guard checker


view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Nov 02 2022 at 19:38):

I think you're right.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:51):

Yes, you're right

view this post on Zulip Notification Bot (Nov 23 2022 at 13:10):

Jason Gross has marked this topic as resolved.


Last updated: Sep 25 2023 at 12:01 UTC