[Agda] function parameters similar to data parameters

Andreas Abel andreas.abel at ifi.lmu.de
Thu Nov 22 11:41:48 CET 2012

On 19.11.2012 10:21, Dominique Devriese wrote:
> 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.

I stumbled over this problem several times myself.  It is a tricky one 
to fix, I have fixed the lhs aspect of it.  See issue 655.

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list