[Agda] irrelevancy annotation

[Carette, Jacques]

Don't use double-negation.  Instead of Null, use an HasElement data-structure.
data HasElement : List A → Set α  where 
  has-elem : (x : A) {xs List A} -> HasElement (x ∷ xs)

Then you need to match on both the list and has-elem enough to reveal the actual head.

I don't know why you want this to be irrelevant though.  Are you sure you don't want a Vec instead of a List?  Lists are best understood as vectors that have forgotten their length. 

Jacques

> -----Original Message-----
> From: Agda <agda-bounces at lists.chalmers.se> On Behalf Of
> mechvel at scico.botik.ru
> Sent: December 21, 2020 4:47 PM
> To: agda at lists.chalmers.se
> Subject: [Agda] irrelevancy annotation
> 
> Please,
> how to fix the following example with irrelevancy denotation?
> 
> module _ {A : Set α}
>    where
>    data Null : List A → Set α  where  isNull : Null []
> 
>    head : (xs : List A) .(nn : ¬ Null xs) → A
>    head (x  _) _  = x
>    head []      nn = contradiction isNull _    -- ?
> 
>    test : ∀ {xs} (nn nn' : ¬Null xs) → head xs nn ≡ head xs nn'
>    test _ _ = refl
> 
> The second pattern in `head` cannot be skipped, but I do not find how to fix it.
> 
> Thanks,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda