This interpreter uses a slightly different grammar that the one you've learned in class, mostly to make it easier to type expressions and to check them.

The grammar is as follows:

        <expression>  ::= <variable>
                       |  <abstraction>
                       |  <application>
        <variable>    ::= α ∈ { a ... z }
	<abstraction> ::= (L<variable>.<expression>)
	<application> ::= (<expression><expression>)
    
The checker always performs the leftmost derivation. For example, the expression (λf.λg.f (g a))(λx.(b x c)) can be typed in as ((Lf.(Lg.(f(ga))))(Lx.((bx)c))). In other words, replace λ with L, surround application and abstraction with parentheses, and remove all whitespace.