Function lambda_calculus::list::foldl

pub fn foldl() -> Term

Applied to a function, a starting value and a Church list it performs a left fold on the list.

FOLDL := Z (λgfex. NULL x (λz.e) (λz.g f (f e (FIRST x)) (SECOND x)) I) = Z (λ λ λ λ NULL 1 (λ 2) (λ 5 4 (4 3 (FIRST 2)) (SECOND 2)) I)

Example

use lambda_calculus::term::Term;
use lambda_calculus::list::{foldl, nil};
use lambda_calculus::arithmetic::plus;
use lambda_calculus::reduction::beta;
use lambda_calculus::reduction::Order::*;

let list = Term::from(vec![1.into(), 2.into(), 3.into()]);

assert_eq!(beta(app!(foldl(), plus(), 0.into(), list ), &Normal, 0), 6.into());
assert_eq!(beta(app!(foldl(), plus(), 0.into(), nil()), &Normal, 0), 0.into());