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.

Sign up for GitHub

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

Jump to bottom

Slow type-checking: replace `admitted` by proof #204

Open

benediktahrens opened this issue Jan 13, 2022 · 0 comments

Member

benediktahrens commented Jan 13, 2022

File https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v contains admitted statements:

TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

Line 44 in 9242475

use weqimplimpl; apply admit_slow_proof.
TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

Line 90 in 9242475

- intros X Y. apply admit_slow_proof. (* refine (pr2 (idweq _)). *)
TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

Line 91 in 9242475

- admit. (* refine (pr2 DiscCompCat_DiscCompCatDef_weq). *)

Fragments or complete proofs are there, but do not type-check in a reasonable amount of time, or at all.

The admitted statements should be proved.

For some background, see also #202 (comment)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment