Function lambda_calculus::combinators::s

pub fn s() -> Term

S - the substitution combinator.

S := λxyz.x z (y z) = λ λ λ 3 1 (2 1)

Example

use lambda_calculus::term::Term;
use lambda_calculus::combinators::s;
use lambda_calculus::reduction::beta_full;

assert_eq!(beta_full(s().app(0.into()).app(1.into()).app(2.into())),
           beta_full(Term::from(0).app(2.into()).app(Term::from(1).app(2.into()))));