[Agda] function application in index positions

[Alan Jeffrey]

In this particular case there's a pretty easy lemma which does the job:

  emptinessProof : ¬ Even 1
  emptinessProof e = lemma e refl where

   lemma : ∀ {n} → Even n → (n ≢ 1)
   lemma (double zero) ()
   lemma (double (suc zero)) ()
   lemma (double (suc (suc m))) ()

More generally, there is some jumping through hoops with propositional 
equality that's often needed, but this is probably easier than trying to 
work out the appropriate notion of definitional equality.

A.

On 02/01/2013 02:32 PM, Peter Divianszky wrote:
> Hi,
>
> Currently it is not easy to deal with function application in index
> positions.
>
> For example, given
>
> \begin{code}
> open import Data.Nat
> open import Relation.Nullary
>
> data Even : ℕ → Set where
>    double : ∀ n → Even (n + n)
>
> emptinessProof : ¬ Even 1
> emptinessProof e = {!!}
> \end{code}
>
> it is not trivial to fill in the hole.
>
> Is it possible to improve to compiler to make this task simpler?
> I don't want to change the data definition.
>
> Is this documented / should I open a ticket?
>
> Thanks,
>
> Peter
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda