Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]

[Thorsten Altenkirch]

On 9 May 2011, at 11:20, Noam Zeilberger wrote:

> If the current notation is seen as a problem, again I would propose
> something like the following, more general since it also allows
> recursive function definitions (but easy to implement given the
> strategy of converting to top-level definitions):
> 
> and = the f { f true x = x ; f false _ = false }
> 
> Such a notation could work for (potentially-recursive) records as well, e.g.,
> 
> pair e1 e2 = the f { fst f = e1 ; snd f = e2 }
> 
> If you want to be explicit that a function/record is non-recursive,
> perhaps you could use a keyword that introduces a dummy name, e.g.,
> 
> and = the# { # true x = x ; # false _ = false }
> 
> There are probably better choices of keywords here than "the" and "the#"...

What about self? (or this) :-)

When using recursive records in our attempts to define omega-categories I often felt the need to refer to the record I am just defining without having to turn it into an explicit definition.

Thorsten