[Agda] function parameters similar to data parameters

[Peter Divianszky]

On 22/11/2012 11:46, Andreas Abel wrote:
> On 19.11.2012 09:57, Peter Divianszky wrote:
>> Now this is possible:
>>
>> ---------------------------------------------------
>> module _ {P : ℕ → Set} (z : P zero) (s : ∀ m → P m → P (suc m)) where
>>    ℕ-elim : ∀ n → P n
>>    ℕ-elim zero = z
>>    ℕ-elim (suc n) = s _ (ℕ-elim n)
>> ---------------------------------------------------
>>
>> My question is, could we write
>>
>> ---------------------------------------------------
>> ℕ-elim {P : ℕ → Set} (z : P zero) (s : ∀ m → P m → P (suc m))
>>         : ∀ n → P n
>> ℕ-elim zero = z
>> ℕ-elim (suc n) = s _ (ℕ-elim n)
>> ---------------------------------------------------
>
> Is this so much more succinct than the section?  I have wondered about
> telescopes for function definitions myself before, but how does this
> scale to mutual functions?

I'm quite happy with sections, but if I go on and use them, I'll end up 
one section per every single function at the end.
In that case telescopes look nicer.

Mutual functions are not that common.
 From another point of view, we have the same situation with data with 
telescopes and mutual data I think.
Why not treat data and function in the same way regarding telescopes?

> We could maybe allow telescopes in mutual with
>
>    mutual tel
>      decls
>
> being a shorthand for
>
>    module _ tel where
>      mutual
>        decls
>