Function lambda_calculus::data::num::binary::shl0

source ·
pub fn shl0() -> Term
Expand description

Applied to a binary-encoded number it shifts it up by a single zero bit.

SHL0 ≡ λnbzo.z (n b z o) ≡ λ λ λ λ 2 (4 3 2 1)

Example

use lambda_calculus::data::num::binary::shl0;
use lambda_calculus::*;

assert_eq!(beta(app(shl0(), 1.into_binary()), NOR, 0), 2.into_binary());
assert_eq!(beta(app(shl0(), 2.into_binary()), NOR, 0), 4.into_binary());
assert_eq!(beta(app(shl0(), 3.into_binary()), NOR, 0), 6.into_binary());