TypeTheory icon indicating copy to clipboard operation
TypeTheory copied to clipboard

Published 20 hours ago • verified publisher icon UniMath

Slow type-checking: replace `admitted` by proof

Open benediktahrens opened this issue 3 years ago • 0 comments

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

  • https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L44
  • https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L90
  • https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L91

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 https://github.com/UniMath/TypeTheory/pull/202#discussion_r784385138

benediktahrens avatar Jan 13 '22 23:01 benediktahrens