Panic: Pattern match failure with Setω and --without-K #6005
Labels
cubical
Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp
internal-error
Concerning internal errors of Agda
regression on master
Unreleased regression in development version (Change to "regression in ..." should it be released!)
set-omega
Problems with infinite sorts (Setω/SSetω)
type: bug
Issues and pull requests about actual bugs
Milestone
There seem to be a regression in the current master of Agda.
The following code (where we define the equality type at Setω)
fails with the following message:
Can confirm this typechecks fine with the latest release (
2.6.2.2
) and with--with-K
.The text was updated successfully, but these errors were encountered: