Stream: MetaCoq

Topic: question about impredicative set


view this post on Zulip Ember Edison (May 03 2021 at 12:53):

Hi, Can I enable Metacoq in Coq -impredicative-set flag?
And Metacoq Safe Checker can check Coq impredicative set code in standard Coq?

view this post on Zulip Théo Winterhalter (May 03 2021 at 12:59):

Setting the flag will not set it for the checker. I don't think we support external flag selection at the moment, and I don't think the checker currently support impredicative Set.
The safe checker is anyway not complete enough to work for most projects. What did you want it for?

view this post on Zulip Ember Edison (May 03 2021 at 14:30):

How many flags are supported? Does metacoq support universe polymorphism now?

view this post on Zulip Théo Winterhalter (May 03 2021 at 14:33):

Yes it supports universe polymorphism, but which part do you want to use? The reification plugin or the safe checker?

view this post on Zulip Théo Winterhalter (May 03 2021 at 14:34):

Here are the flags that we currently have internally: https://github.com/MetaCoq/metacoq/blob/coq-8.13/template-coq/theories/config.v#L4

view this post on Zulip Ember Edison (May 03 2021 at 14:40):

thank you.

view this post on Zulip Théo Winterhalter (May 03 2021 at 14:41):

If you would need another one, feel free to open an issue.

view this post on Zulip Ember Edison (May 04 2021 at 05:51):

In my memory, impredicative set support was added in the metacoq milestone of the ancient version. Am I wrong?

view this post on Zulip Théo Winterhalter (May 04 2021 at 06:14):

I don't remember this but maybe @Matthieu Sozeau knows.

view this post on Zulip Matthieu Sozeau (May 04 2021 at 06:52):

We don't have support for impredicative set yet, but that should be relatively easy to add.


Last updated: Aug 11 2022 at 02:03 UTC