[Agda] question on irrelevant argument

[Ulf Norell]

You can define an irrelevant version of ⊥-elim which you can use in foo2
and foo3:

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

/ Ulf


On Sun, Jan 19, 2014 at 2:50 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> Please,
> how to fix  foo2, foo3  shown below?
>
> ----------------------------------------------------------------
> open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
> open import Data.Empty using (⊥-elim)
> open import Data.Nat   using (ℕ; module ℕ)
>
> open ℕ
>
> foo : (m n : ℕ) → n ≢ zero → ℕ             -- this works
> foo _ (suc n) _  =  n
> foo _ zero    nz =  ⊥-elim (nz PE.refl)
>
>
> foo2 : (m n : ℕ) → .(n ≢ zero) → ℕ
> foo2 _ (suc n) _ =  n
> foo2 _ zero    _ =  ⊥-elim (u PE.refl)     -- is not type-checked
>                     where
>                     u : zero ≢ zero
>                     u = _
> {-
> foo3 : (m n : ℕ) → .{nz : n ≢ zero} → ℕ
> foo3 _ (suc n) {_} =  n
> foo3 _ zero    {_} =  ⊥-elim (u PE.refl)      -- is not type-checked
>                       where
>                       u : zero ≢ zero
>                       u = {!!}
> -}
> ---------------------------------------------------------------------
>
> The checker   (of  development Agda of January 8, 2014)
>
> does not allow to skip the `zero' branch, nor to set () there,
> nor to apply  ⊥-elim
> (nz  is rejected for  u,  as well as '_').
>
> 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/20140119/8eeed857/attachment.html