* returning results in combinator form (the evaluator already accepts combinators as input)
* displaying reductions one step at a time
* specifying the reduction order and depth
-* allow other binders such as ∀ and &exists; (though these aren't interpreted as doing anything other than binding variables)
+* allow other binders such as ∀ and ∃ (though these aren't interpreted as doing anything other than binding variables)
Other Lambda Evaluators/Calculutors
-----------------------------------