[−][src]Function lambda_calculus::data::num::stumpfu::to_scott
pub fn to_scott() -> Term
Applied to a Stump-Fu-encoded number it produces the equivalent Scott-encoded number.
TO_SCOTT ≡ λn.(λm.m SCOTT_SUCC SCOTT_ZERO) (n TRUE n) ≡ λ (λ 1 SCOTT_SUCC SCOTT_ZERO) (1 TRUE 1)
Example
use lambda_calculus::data::num::stumpfu::to_scott; use lambda_calculus::*; assert_eq!(beta(app(to_scott(), 0.into_stumpfu()), NOR, 0), 0.into_scott()); assert_eq!(beta(app(to_scott(), 1.into_stumpfu()), NOR, 0), 1.into_scott()); assert_eq!(beta(app(to_scott(), 4.into_stumpfu()), NOR, 0), 4.into_scott());