Buggy STLC example?

[gallais]

While working on https://github.com/gallais/agdarky I've noticed that the parser for STLC I had did not work on examples of the form \f.\a.\b. f a b which would get parsed as \f.\a.\b. f (a b) rather than \f.\a.\b. (f a) b. I have pushed a fix on agdarky but haven't had the time to look back at the example we have here (and in the agdarsec repo).

The idea behind the fix amounts to:

• the head of the neutral term is either a variable, a cut or an infer between parentheses
• each argument is either a variable or a whole checkable term in parentheses

[clayrat]

Oh I think I actually ran into this when adapting this example for PCF, but I thought I did something wrong. I'll try to adapt your fix next week!

[gallais]

I've pushed a fix to agdarsec. It should be easier to port than the agdarky one which also includes the introduction of a lexer.