Function lambda_calculus::data::num::signed::sub

pub fn sub(encoding: Encoding) -> Term

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

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

Example

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

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