(you can use "\" instead of "λ")
Examples:
λxyz.xz(yz)
λxyz.(λu.xzu)(yz)
λx.xx
(λx.xx)λx.xx
λfx.f(fx)
(λfx.f(fx))λfx.f(fx)
Click on a redex (in blue):
Show formulas
Show terms
(clicking on an atomic formula or a variable focuses the corresponding label)