Function lambda_calculus::data::num::stumpfu::pred

source ·

pub fn pred() -> Term

Expand description

Applied to a Stump-Fu-encoded number it produces its predecessor.

PRED ≡ λn.n (λcs.s) ZERO ≡ λ 1 (λ λ 1) ZERO

Example

use lambda_calculus::data::num::stumpfu::pred;
use lambda_calculus::*;

assert_eq!(beta(app(pred(), 1.into_stumpfu()), NOR, 0), 0.into_stumpfu());
assert_eq!(beta(app(pred(), 3.into_stumpfu()), NOR, 0), 2.into_stumpfu());