[Agda] Lambda

[Edward Kmett]

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.

http://www.cs.ru.nl/~janz/yarrow/userg.html#binder

Then you could define the unicode lambda as a binder version of the
identity function in a library and not have to modify the core syntax.

This would then enable the use of lambda for other purposes, as long
as they don't import that library. You can also implement a lot of
other variable binding constructs with this notation as well.

-Edward

On Thu, Jun 19, 2008 at 9:53 AM, Nils Anders Danielsson
<nils.anders.danielsson at gmail.com> wrote:
> On Wed, Jun 18, 2008 at 4:14 PM, Samuel Bronson <naesten at gmail.com> wrote:
>
>> On Wed, Jun 18, 2008 at 9:54 AM, Lennart Augustsson
>> <lennart at augustsson.net> wrote:
>>
>>> E.g., if I were doing physics programming in Agda I'd want to use
>>> lambda for wavelengths.
>>
>> Or... say you were formalizing a variant of lambda calculus?
>
> I have used λ when formalising lambda calculi. Still I think that the
> only reasonable replacement of \ for the lambda of the meta language
> is λ, since this is probably the lambda that will be written and read
> most often by Agda users. For my object languages I can imagine using
> something like ƛ.
>
> --
> /NAD
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>