Function lambda_calculus::data::num::signed::to_signed

source ·

pub fn to_signed(encoding: Encoding) -> Term

Expand description

Applied to a numeral with a specified encoding it produces a pair representing its signed equivalent.

TO_SIGNED ≡ λx.PAIR x ZERO ≡ λ PAIR 1 ZERO

Example

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

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