Function lambda_calculus::data::num::binary::strip

pub fn strip() -> Term

Applied to a binary-encoded number it strips its leading zeroes.

STRIP ≡ λn.FST (n Z A B) ≡ λ FST (n Z A B)

where

Z ≡ PAIR ZERO TRUE

A ≡ λp.p (λnz.PAIR (z ZERO (SHL0 n)) z) ≡ λ 1 (λ λ PAIR (1 ZERO (SHL0 2)) 1)

B ≡ λp.p (λnz.PAIR (SHL1 n) FALSE) ≡ λ 1 (λ λ PAIR (SHL1 2) FALSE)

Example

use lambda_calculus::data::num::binary::{strip, shl0};
use lambda_calculus::*;

let zero_with_a_leading_zero = beta(app(shl0(), 0.into_binary()), NOR, 0);

assert_eq!(
    beta(app(strip(), zero_with_a_leading_zero), NOR, 0),
    0.into_binary()
);