Function lambda_calculus::combinators::iota

pub fn iota() -> Term

Iota - the universal combinator.

ι := λx.x S K = λ 1 S K

Example

use lambda_calculus::combinators::{iota, i, k, s};
use lambda_calculus::reduction::beta_full;

assert_eq!(beta_full(iota().app(iota())), i());
assert_eq!(beta_full(iota().app(iota().app(iota().app(iota())))), k());
assert_eq!(beta_full(iota().app(iota().app(iota().app(iota().app(iota()))))), s());