[Agda] Lambda

[Nils Anders Danielsson]

On Thu, Jun 19, 2008 at 4:21 PM, Edward Kmett <ekmett at gmail.com> wrote:
>
> One approach that could handle this case, which I haven't seen
> anywhere else is the approach used in Jan Zwanenburg's Yarrow for
> defining new binders.

We have considered adding something like this. However, it's not clear
that it is a good thing to make the syntax more complex.

Note, by the way, that there are facilities for defining binders in
both Coq and Isabelle. See also Missura's PhD thesis, Higher-Order
Mixfix Syntax for Representing Mathematical Notation and its Parsing
(http://www.inf.ethz.ch/research/disstechreps/theses/show?serial=12108&lang=en).

-- 
/NAD