Function lambda_calculus::arithmetic::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 := Y (λgqab.LT a b (PAIR q a) (g (SUCC q) (SUB a b) b)) ZERO = Y (λ λ λ λ LT 2 1 (PAIR 3 2) (4 (SUCC 3) (SUB 2 1) 1)) ZERO

Example

use lambda_calculus::arithmetic::div;
use lambda_calculus::term::Term;
use lambda_calculus::reduction::beta_full;

assert_eq!(beta_full(div().app(3.into()).app(2.into())),
           Term::from((1.into(), 1.into())));