[Agda] irrelevancy annotation

[mechvel at scico.botik.ru]

On 2020-12-22 11:51, Ulf Norell wrote:
> This should work:
> 
> contradiction : .⊥ → A
> contradiction ()
> 
> head : (xs : List A) .(nn : ¬ Null xs) → A
> head (x ∷ _) _  = x
> head []      nn = contradiction (nn isNull)


I see. Thank you.

In about 2014, I had an unlucky experience with using irrelevancy 
annotation,
have been stuck with type checking.
Does anybody use successfully irrelevancy annotation?

Thanks,

--
SM