Function lambda_calculus::data::list::pair::zip_with

pub fn zip_with() -> Term

Applied to a function and two pair-encoded lists it applies the function to the corresponding elements and returns the resulting list. If one input list is shorter, excess elements of the longer list are discarded.

ZIP_WITH ≡ Z (λzfab.IS_NIL b (λx.NIL) (λx.IS_NIL a NIL (CONS (f (HEAD b) (HEAD a)) (z f (TAIL b) (TAIL a)))) I) ≡ Z (λ λ λ λ IS_NIL 2 (λ NIL) (λ IS_NIL 2 NIL (CONS (4 (HEAD 3) (HEAD 2)) (5 4 (TAIL 3) (TAIL 2)))) I)

Example

use lambda_calculus::data::list::pair::zip_with;
use lambda_calculus::data::num::church::add;
use lambda_calculus::*;

let list1 = || vec![2.into_church(), 3.into_church()].into_pair_list();
let list2 = || vec![4.into_church(), 6.into_church()].into_pair_list();

assert_eq!(beta(app!(zip_with(), add(), list1(), list1()), NOR, 0), list2());