Instructions
- evaluate λ-expressions (see grammer)
- add λ-terms to context (<id> [:t <type>] = <term>)
- remove λ-terms from context (del <id>)
Grammar rules
- any identifier is a λ-term
- true and false are λ-term of type Bool
- zero is a λ-term of type Nat
- given identifier x and a λ-term t: λx:Type.t is a λ-term
- given two λ-terms: t1 of type A -> B and t2 of type A: (t1 t2) is a λ-term of type B
- given cond of type Bool and t1, t2 λ-terms of the same type: if cond then t1 else t2 is a λ-term
- given t of type Nat: succ t, pred t, iszero t are λ-terms
- given t1 and t2, both of type Nat: plus t1 t2, minus t1 t2 are λ-terms
Features
- type "\" to get "λ"
- enable Verbouse option to see the step-by-step evaluation
- "clear" to clear the terminal
- Up/Down to navigate previous commands