Function lambda_calculus::data::num::signed::add

pub fn add(encoding: Encoding) -> Term

Applied to two signed integers with a specified encoding it returns a signed integer equal to their sum.

ADD ≡ λab.SIMPLIFY (PAIR (ADD (FST a) (FST b)) (ADD (SND a) (SND b))) ≡ λ λ SIMPLIFY (PAIR (ADD (FST 2) (FST 1)) (ADD (SND 2) (SND 1)))

Example

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

assert_eq!(
    beta(app!(add(Church), (-1).into_signed(Church), 3.into_signed(Church)), NOR, 0),
    beta(2.into_signed(Church), NOR, 0)
);