foldr

Function foldr 

Source
pub fn foldr() -> Term
Expand description

Applied to a function, a starting value and a pair-encoded list it performs a right fold on the list.

FOLDR ≡ λfal.Z (λzt.IS_NIL t (λx.a) (λx.f (HEAD t) (z (TAIL t))) I) l ≡ λ λ λ Z (λ λ IS_NIL 1 (λ 5) (λ 6 (HEAD 2) (3 (TAIL 2))) I) 1

§Example

use lambda_calculus::data::list::pair::foldr;
use lambda_calculus::data::num::church::{add, sub};
use lambda_calculus::*;

let list = || vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();

assert_eq!(beta(app!(foldr(), add(), 0.into_church(), list()), NOR, 0), 6.into_church());
assert_eq!(beta(app!(foldr(), sub(), 6.into_church(), list()), NOR, 0), 0.into_church());