Function lambda_calculus::data::num::signed::mul

pub fn mul(encoding: Encoding) -> Term

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

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

Example

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

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