Function lambda_calculus::data::num::parigot::pred

source ·

pub fn pred() -> Term

Expand description

Applied to a Parigot-encoded number it produces its predecessor.

PRED ≡ λn.n (λxy.y) ZERO ≡ λ 1 (λ λ 1) ZERO

Example

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

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