[Agda] function parameters similar to data parameters

[Andreas Abel]

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?

We could maybe allow telescopes in mutual with

   mutual tel
     decls

being a shorthand for

   module _ tel where
     mutual
       decls


-- 
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
http://www2.tcs.ifi.lmu.de/~abel/