Function lambda_calculus::data::num::scott::add

pub fn add() -> Term

Applied to two Scott-encoded numbers it produces their sum.

ADD ≡ Z (λfmn.m n (λo. SUCC (f o n))) ≡ Z (λ λ λ 2 1 (λ SUCC (4 1 2)))

Example

use lambda_calculus::data::num::scott::add;
use lambda_calculus::*;

assert_eq!(beta(app!(add(), 1.into_scott(), 2.into_scott()), NOR, 0), 3.into_scott());
assert_eq!(beta(app!(add(), 2.into_scott(), 3.into_scott()), NOR, 0), 5.into_scott());

Errors

This function will overflow the stack if used with an applicative-family (APP or HAP) reduction order.