UlfNorell
commented
10 years ago From andreas....@gmail.com on November 05, 2013 04:30:33
Interesting --- have not thought about the connection to irrelevance yet...
Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Milestone-2.3.4 Copatterns Irrelevance
From Daniel.G...@gmail.com on November 05, 2013 13:19:27
What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). {-# OPTIONS --copatterns #-} module Bug where
record Sigma (A : Set)(P : A → Set) : Set where field fst : A .snd : P fst open Sigma
postulate A : Set P : A → Set x : A .p : P x
ex : Sigma A P ex = record { fst = x ; snd = p }
ex' : Sigma A P fst ex' = x snd ex' = {!p!}
Giving p yields the following error: Identifier p is declared irrelevant, so it cannot be used here when checking that the expression p has type P (fst ex') What version of Agda are you using? On what operating system (if relevant)? Latest Darcs
Original issue: http://code.google.com/p/agda/issues/detail?id=939