12
data _≅_ {A : Set} (x : A) : ∀ {B : Set} → B → Set where
15
record Σ (A : Set) (B : A → Set) : Set where
23
data Bool : Set where true false : Bool
25
data D : Bool -> Set where
30
P S = Σ S (\s → s ≅ tt)
35
¬pbool2 : ¬ P (D false)
37
{- WAS: expected error
38
ff ≅ tt should be empty, but that's not obvious to me
39
when checking that the clause ¬pbool2 (ff , ()) has type