Function lambda_calculus::arithmetic::quot

pub fn quot() -> Term

Applied to two Church-encoded numbers it returns a Church-encoded quotient of their division.

QUOT := Y (λrab.LT a b ZERO (SUCC (r (SUB a b) b))) = Y (λ λ λ LT 2 1 ZERO (SUCC (3 (SUB 2 1) 1)))

Example

use lambda_calculus::arithmetic::quot;
use lambda_calculus::reduction::beta_full;

assert_eq!(beta_full(quot().app(6.into()).app(2.into())), 3.into());