Hi, Can I enable Metacoq in Coq -impredicative-set flag?
And Metacoq Safe Checker can check Coq impredicative set code in standard Coq?
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
The safe checker is anyway not complete enough to work for most projects. What did you want it for?
How many flags are supported? Does metacoq support universe polymorphism now?
Yes it supports universe polymorphism, but which part do you want to use? The reification plugin or the safe checker?
Here are the flags that we currently have internally: https://github.com/MetaCoq/metacoq/blob/coq-8.13/template-coq/theories/config.v#L4
If you would need another one, feel free to open an issue.
In my memory, impredicative set support was added in the metacoq milestone of the ancient version. Am I wrong?
I don't remember this but maybe @Matthieu Sozeau knows.
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