I found the syntax in the book Types and Programming Languages - from here on referred to as TaPL. It is as simple as the language. The grammar consists of terms that can be either abstractions, applications or variables. I have added a let statement so that terms can be bound as done in F# or JavaScript. The full grammar in the syntax of Grammar2Slr is as follows
token "eq" ,"lambda" ,"dot" as "=" ,"\\\\" ,"." token "lpar" ,"rpar" ,"scolon" as "(" ,")" ,";" token "let" as "let" token -cap "var" as "[a-zA-Z0-9_\\-]+" !token " " # Productions prod Stmt -> Def "scolon" Stmt | Term0 # Definintions are done first thing in the program prod Def -> "let" "var" "eq" Term0 # Both associativity and precedence are directly done in grammar # Hence the numbering of the terms, 0,1,2 for low,mid,hight prec, resp. prod Term0 -> "lambda" "var" "dot" Term0 | Term1 prod Term1 -> Term1 Term2 | Term2 prod Term2 -> "var" | "lpar" Term0 "rpar"As noted in the comments we don't need to explicitly state precedence or associativity with a grammar like this. We can add these by construction of the grammar.
I have stolen the \, used to denote the λ symbol, from Haskell. The two look somewhat a like. So \ in this language is λ. The dot . has the exact same meaning as in TaPL.
Terms can be parenthesized - this is not explicitly stated in TaPL, but it is needed in order to apply within the body of an abstraction. Application binds tighter than abstraction. Application is left associative, abstraction right.
Variable names can be some combination of lower case letters, upper case, integers, - or _. Id-tokens could be as liberal as with the BoxProver project, but I have made this restriction for what ever reason.
The let @ = term ; has to end with a semicolon.
And that is it.