# [Agda] function application in index positions

Alan Jeffrey ajeffrey at bell-labs.com
Fri Feb 1 22:15:20 CET 2013

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