Function lambda_calculus::data::list::pair::take_while

pub fn take_while() -> Term

Applied to a predicate function and a pair-encoded list it returns the longest prefix of the list whose elements all satisfy the predicate function.

TAKE_WHILE ≡ Z (λzfl. IS_NIL l (λx.NIL) (λx.f (HEAD l) (CONS (HEAD l) (z f (TAIL l))) NIL) I) ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ 3 (HEAD 2) (CONS (HEAD 2) (4 3 (TAIL 2))) NIL) I)

Example

use lambda_calculus::data::list::pair::take_while;
use lambda_calculus::data::num::church::is_zero;
use lambda_calculus::*;

let list1 = vec![0.into_church(), 0.into_church(), 1.into_church()].into_pair_list();
let list2 = vec![0.into_church(), 0.into_church()].into_pair_list();

assert_eq!(beta(app!(take_while(), is_zero(), list1), NOR, 0), list2);