[Agda] using irrelevant field

[Andreas Abel]

The example is rejected since the proof x/=0 is irrelevant in (subEl x 
x/=0), but f expects it to be relevant.

The fix 2. is correct.

The other way to fix it is of course to just drop the second argument to 
f, since it is unused anyway.

Probably your example is too simplistic, you want to do something more 
advanced with irrelevance!?

Cheers,
Andreas

On 17.03.2014 19:40, Sergei Meshveliani wrote:
> People,
> consider the program
>
> ---------------------------------------
> open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
> open import Data.Nat using (ℕ; suc)
>
> record Nonzero : Set where  constructor subEl
>                              field  elem   : ℕ
>                                     .proof : elem ≢ 0
> f : (x : ℕ) → x ≢ 0 → ℕ
> f x _ =  suc x
>
> g : Nonzero → ℕ
> g (subEl x x≢0) =  f x x≢0
> ---------------------------------------
>
> It is not type-checked
> (in Development Agda of February 16, 2014).
>
> 1. Is this all right?
>
> 2. This can be fixed by making irrelevant the second argument in  f.
> Is this the only way to fix?
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/