The failing test for #6060 succeeds if we change Prop for Propω:
{-# OPTIONS --cubical --prop -WnoUnsupportedIndexedMatch #-}
open import Agda.Primitive
open import Agda.Builtin.Equality
data S : Set where s : S
data P : Propω where p : P
-- The following is rejected for P : Prop
-- so should also be rejected for P : Propω.
g : (x : S) → s ≡ x → P → S
g .s refl y = s
Propω was added in 2.6.4, but apparently not correctly in its interaction with Cubical Agda.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4