Parse Nominal Definitions

[bash]

Syntax is very similar to schematic definitions

True -> (λt f.t)
False -> (λt f.f)

Definitions may reference other definitions but they may not be mutually recursive to prevent infinite loops while expanding definitions. (You should use a Y-combinator if you need mutual recursion)

[bash]

Alternative plan: Definitions can only reference previously defined definitions. This is a lot easier to validate and I could then allow definitions inside formulas to have some sort of let x = y statements.

[bash]

\f x .
    y -> (x x)
    f y

is translated to:

\f x .
    (\y . f y)  
    (x x)

This has the advantage that I'm only introducing syntax sugar, not new functionality.

[bash]

implemented in d5d546fae70639f0d71fb2ee2a04e37c00e0749e