Function lambda_calculus::booleans::and

pub fn and() -> Term

Applied to two Church-encoded booleans it returns their Church-encoded conjunction.

AND := λpq.p q p = λ λ 2 1 2

Examples

use lambda_calculus::booleans::{and, tru, fls};
use lambda_calculus::reduction::beta;
use lambda_calculus::reduction::Order::*;

assert_eq!(beta(app!(and(), tru(), tru()), &Normal, 0), tru());
assert_eq!(beta(app!(and(), tru(), fls()), &Normal, 0), fls());
assert_eq!(beta(app!(and(), fls(), tru()), &Normal, 0), fls());
assert_eq!(beta(app!(and(), fls(), fls()), &Normal, 0), fls());