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::normalize;

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