Function lambda_calculus::data::num::church::div

pub fn div() -> Term

Applied to two Church-encoded numbers it returns a Church-encoded pair with the result of their division - the quotient and the remainder.

DIV ≡ Z (λzqab.LT a b (λx.PAIR q a) (λx.z (SUCC q) (SUB a b) b) I) ZERO ≡ Z (λ λ λ λ LT 2 1 (λ PAIR 4 3) (λ 5 (SUCC 4) (SUB 3 2) 2) I) ZERO

Example

use lambda_calculus::data::num::church::div;
use lambda_calculus::*;

assert_eq!(
    beta(app!(div(), 4.into_church(), 2.into_church()), NOR, 0),
    (2, 0).into_church()
);
assert_eq!(
    beta(app!(div(), 5.into_church(), 3.into_church()), NOR, 0),
    (1, 2).into_church()
);

Errors

This function will loop indefinitely if the divisor is zero().