rem

lambda_calculus::data::num::church

Function rem 

Source 
pub fn rem() -> Term
Expand description

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

REM ≡ Z (λzab.LT a b (λx.a) (λx.z (SUB a b) b) I) ≡ Z (λ λ λ LT 2 1 (λ 3) (λ 4 (SUB 3 2) 2) I)

§Example

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

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

§Errors

This function will loop indefinitely if the second argument is zero()