Instances defined outside the opaque block sometimes fail to resolve when inside. Possibly some issue with the discrimination trees (ping @plt-amy). Works on 2.6.4.3.
it : {A : Set} → ⦃ A ⦄ → A
it ⦃ x ⦄ = x
postulate
X : Set
C : Set → Set
c : {A : Set} → ⦃ C A ⦄ → A
opaque
Y : Set
Y = X
instance
postulate CY : C Y
opaque
unfolding Y
works : Y
works = c ⦃ it ⦄
fails : Y
fails = c
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