[Agda] AIM XIII code sprints

[Andreas Abel]

Hi Karim,

thanks for your message.

On 5/4/11 5:02 PM, karim kanso wrote:
> On behalf of Noam and Fredrick.
>
> We have spend some more time working on an extended syntax for lambda
> expressions. It is currently
> at status 3. The use of with and where clauses have issues, the where
> clauses have lambda lifting
> issues, with clauses have scoping issues.
>
> We could submit a beta patch that will allow for anonymous case
> distinctions, but disable the use of with
> and where clauses inside the lambda terms for now?

That is already something!

Could you explain what the syntax now is for the lambda with matching?

Cheers,
Andreas

> On 28 April 2011 15:30, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     Hi AIM XIII participants,
>
>     two weeks after the end of this very successful meeting, I would
>     like to know the status of the code sprints which were continued
>     after the meeting.
>
>     @Makoto: I do not remember all the sprints, can I find the notes
>     online somewhere?
>
>     Status:
>       1 = finished
>       2 = almost finished
>       3 = still working, might take some more time
>       4 = indefinitely postponed
>       5 = abandoned
>
>     Sprint                           Leader            Status
>
>       clean up builtins              Simon             1?
>       unquote                        Nicolas           3?
>       first class lambda syntax      Noam               ?
>       mutual blocks                  James             3?
>       installer                      Makoto             ?
>       meta variables                 Andreas           3
>
>       what else?
>
>     Cheers,
>     Andreas
>
>     --
>     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 <mailto:andreas.abel at ifi.lmu.de>
>     http://www2.tcs.ifi.lmu.de/~abel/ <http://www2.tcs.ifi.lmu.de/%7Eabel/>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>

-- 
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/