Function lambda_calculus::data::num::signed::modulus

source ·

pub fn modulus(encoding: Encoding) -> Term

Expand description

Applied to a signed integer with a specified encoding it returns its unsigned absolute value.

MODULUS ≡ λx.(λy.IS_ZERO (FST y) (SND y) (FST y)) (SIMPLIFY x) ≡ λ (λ IS_ZERO (FST 1) (SND 1) (FST 1)) (SIMPLIFY 1)

Example

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

assert_eq!(beta(app(modulus(Church),    1.into_signed(Church)), NOR, 0), 1.into_church());
assert_eq!(beta(app(modulus(Church), (-1).into_signed(Church)), NOR, 0), 1.into_church());