Implement section syntax or parameterized modules.

[Toxaris]

To avoid long repetitive parameter lists.

[Toxaris]

Proposal. Desugar this:

forall (x y : A) (z : B) {
  foo = z;
  bar (a b : A) = foo;
}

to this:

foo (x y : A) (z : B) = z;
bar (x y : A) (z : B) (a b : A) = foo x y z;

[Blaisorblade]

:+1:

IIUC, forall seems equivalent to Agda's module _. Reusing an existing design, which we even found useful, would be good.

[Toxaris]

Yes, both my forall above and Agda's module _ are inspired by Coq's section mechanism. See discussion on the Agda issue tracker.