[Agda] irrelevant arg example

[Ulf Norell]

I'm not sure what the different behaviour you are getting is (can you
elaborate?), but f can be implemented as follows:

⊥-elim-irr : .⊥ → ∀ {a} {A : Set a} → A
⊥-elim-irr ()

f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0
f x nz z = ⊥-elim-irr (nz z)

Under normal circumstances irrelevant things cannot be used in relevant
contexts, but one exception is that you are allowed absurd elimination of
irrelevant empty types into relevant types.

/ Ulf



On Wed, Aug 20, 2014 at 1:49 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear Agda developers,
>
> Agda of August 19 2014  type-checks irrelevant arguments in a different
> way than  Agda-2.4.0.2.
> So that some of my code is not type-checked any more.
> I have the two questions on the subject.
>
> 1. Which treating is more correct?
>
> 2. For example, how to implement the function
>
>   f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0
>   f x ???
>
> ?
>
> 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/20140820/2c5238d7/attachment.html