Function lambda_calculus::booleans::not

pub fn not() -> Term

Applied to a Church-encoded boolean it returns its Church-encoded negation.

NOT := λp.p FALSE TRUE = λ 1 FALSE TRUE

Examples

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

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