*Abbreviations*: In an earlier version, you couldn't use abbreviations. `\x y. y x x` had to be written `(\x (\y ((y x) x)))`. We've upgraded the parser though, so now it should be able to understand any lambda term that you can.
-*Constants*: The combinators `S`, `K`, `I`, `C`, `B`, `W`, `T`, `M` (aka <code>ω</code>) and `L` are pre-defined to their standard values. Also, integers will automatically be converted to Church numerals. (`0` is `\s z. z`, `1` is `\s z. s z`, and so on.)
+*Constants*: The combinators `S`, `K`, `I`, `C`, `B`, `W`, `T`, `V`, `M` (aka <code>ω</code>) and `L` are pre-defined to their standard values. Also, integers will automatically be converted to Church numerals. (`0` is `\s z. z`, `1` is `\s z. s z`, and so on.)
*Variables*: Variables must start with a letter and can continue with any sequence of letters, numbers, `_`, `-`, or `/`. They may optionally end with `?` or `!`. When the evaluator does alpha-conversion, it may change `x` into `x'` or `x''` and so on. But you should not attempt to use primed variable names yourself.
constant("B", make_lam3(u, v, x, make_app(uu, make_app(vv, xx))));
constant("C", make_lam3(u, v, x, make_app3(uu, xx, vv)));
- // trush \uv.vu = CI
+ // trush \uv.vu = CI = box
constant("T", make_lam2(u, v, make_app(vv, uu)));
- // mockingbird \u.uu = SII
- constant("M", make_lam(u, make_app(uu, uu)));
+ // vireo \uvw.wuv = pair
+ constant("V", make_lam3(u, v, x, make_app3(xx, uu, vv)));
// warbler \uv.uvv = C(BM(BBT) = C(BS(C(BBI)I))I
constant("W", make_lam2(u, v, make_app3(uu, vv, vv)));
+ // mockingbird \u.uu = SII = omega
+ constant("M", make_lam(u, make_app(uu, uu)));
// lark \uv.u(vv) = CBM = BWB
constant("L", make_lam2(u, v, make_app(uu, make_app(vv, vv))));
// Y is SLL