Agda-2.3.2.2: test/fail/IrrelevantData.agda
-- {-# OPTIONS -v tc.lhs:100 #-}
module IrrelevantData where
data T (A : Set) : Set where
c : .A → T A
d : ∀ {A} → T A → A
d (c x) = x
-- needs to fail since x is irrelevant under c-- {-# OPTIONS -v tc.lhs:100 #-}
module IrrelevantData where
data T (A : Set) : Set where
c : .A → T A
d : ∀ {A} → T A → A
d (c x) = x
-- needs to fail since x is irrelevant under c