[Agda] function parameters similar to data parameters

Dominique Devriese dominique.devriese at cs.kuleuven.be
Mon Nov 19 10:21:08 CET 2012

Peter, all,

2012/11/19 Peter Divianszky <divipp at gmail.com>:
> I conclude this because
> ---------------------------------------------------
> ℕ-elim : {P : ℕ → Set} (z : P zero) (s : ∀ {m} → P m → P (suc m))
>        → ∀ n → P n
> ℕ-elim z s zero = z
> ℕ-elim z s (suc n) = s (ℕ-elim z s n)
> ---------------------------------------------------
> is not allowed now ("Refuse to construct infinite term ..." error),

For clarity, the problem here is that the second s in the expression
"s (ℕ-elim z s n)" has its hidden argument instantiated. It is in fact
equivalent to "s {_}". This is correct behaviour with respect to how
hidden arguments are supposed to behave.  You can fix the error by
preventing the hidden argument from being instantiated by replacing
"s" by its eta-expansion "\ {m} -> s {m}".

I don't have an opinion about Peter's proposal, just wanted to point
out what the problem here is.


More information about the Agda mailing list