[Agda] irrelevancy annotation

[Ulf Norell]

This should work:

contradiction : .⊥ → A
contradiction ()

head : (xs : List A) .(nn : ¬ Null xs) → A
head (x ∷ _) _  = x
head []      nn = contradiction (nn isNull)

/ Ulf

On Mon, Dec 21, 2020 at 10:47 PM <mechvel at scico.botik.ru> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201222/1dfbeeb3/attachment.html>