-
Andrei Paskevich authored
Two points for discussion: - t_lambda accepts both terms and formulas for the body. Thus, t_open_lambda, t_app_lambda, and t_app_beta can all return a term or a formula, depending on what is inside the lambda term. The caller should not forget to check. We could, in principle, always return a term (bool-typed when needed), which would exclude a possible run-time error, but then a caller who expects a formula, would have to recognize the results of the form [if f then True else False], before blindly attaching [== True] to them. Maybe still worth it: it's better if a forgotten check leads to an inefficient formula than to a type-checking error. - t_lambda takes a preid which will be the binding variable in the produced epsilon. This permits us to give names to our lambdas if we want it (what for?) and to give locations to intermediate terms inside the epsilon. Overall, it's not very useful and can probably be removed.
235fac91