Function lambda_calculus::data::num::church::mul

source ·
pub fn mul() -> Term
Expand description

Applied to two Church-encoded numbers it yields their product.

MUL ≡ λmnf.m (n f) ≡ λ λ λ 3 (2 1)

Example

use lambda_calculus::data::num::church::mul;
use lambda_calculus::*;

assert_eq!(beta(app!(mul(), 1.into_church(), 2.into_church()), NOR, 0), 2.into_church());
assert_eq!(beta(app!(mul(), 2.into_church(), 3.into_church()), NOR, 0), 6.into_church());