Function lambda_calculus::combinators::s
[−]
[src]
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()))));