[Agda] function application in index positions

Peter Divianszky divipp at gmail.com
Fri Feb 1 21:32:32 CET 2013


Currently it is not easy to deal with function application in index 

For example, given

open import Data.Nat
open import Relation.Nullary

data Even : ℕ → Set where
   double : ∀ n → Even (n + n)

emptinessProof : ¬ Even 1
emptinessProof e = {!!}

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?



More information about the Agda mailing list