Ember Edison (May 03 2021 at 12:53): 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?
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?
Ember Edison (May 03 2021 at 14:30):How many flags are supported? Does metacoq support universe polymorphism now?
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?
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
Ember Edison (May 03 2021 at 14:40):thank you.
Théo Winterhalter (May 03 2021 at 14:41):If you would need another one, feel free to open an issue.
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?
Théo Winterhalter (May 04 2021 at 06:14):I don't remember this but maybe @Matthieu Sozeau knows.
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: Jun 01 2023 at 12:01 UTC