-
Notifications
You must be signed in to change notification settings - Fork 632
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Anomaly "in Lemmas.save_lemma_admitted: more than one statement." with Derive #18951
Comments
coq/ceps#89 suggests that by postponing the computation of universes from before |
I don't think the error is about universes. |
Sorry, there was an implicit in my message namely that what apparently forced the restriction to one entry is that the current API expects only one universe entry, so if |
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
This includes: - supporting implicit arguments - supporting universe polymorphism - fixing coq#18951: Admitted for Derive TODO: pass definition attributes.
Should be a regular error "Admitted does not support multiple statements" as is done in save_lemma_admitted_delayed
(in fact the delayed case should be the anomaly as multi statement proofs do not support delaying)
The text was updated successfully, but these errors were encountered: