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


Last updated: Jan 30 2023 at 19:04 UTC