[Agda] irrelevancy annotation

[mechvel at scico.botik.ru]

On 2020-12-22 01:04, Carette, Jacques wrote:
> 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.
> [..]


Yes. This way it looks better:

   data HasElement : List A → Set α
        where
        hasElem : (x : A) {xs : List A} → HasElement (x ∷ xs)

   head' : (xs : List A) → .(he : HasElement xs) → A
   head' (x ∷ _) _  = x

   test : ∀ {xs} (nn nn' : HasElement xs) → head' xs nn ≡ head' xs nn'
   test _ _ = refl

The second pattern in head' is now omitted.
But the proof-relevance effect still needs some treating, because 
without the `dot',
`test' is not proved by  refl.

--
SM