Function lambda_calculus::data::list::pair::drop

pub fn drop() -> Term

Applied to a Church-encoded number n and a pair-encoded list it returns a new list without the first n elements of the supplied list.

DROP ≡ Z (λznl.IS_NIL l (λx.NIL) (λx.IS_ZERO n l (z (PRED n) (TAIL l))) I) ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ IS_ZERO 3 2 (4 (PRED 3) (TAIL 2))) I)

Example

use lambda_calculus::data::list::pair::drop;
use lambda_calculus::*;

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

assert_eq!(
    beta(app!(drop(), 1.into_church(), list.into_pair_list()), NOR, 0),
    vec![2.into_church(), 3.into_church()].into_pair_list()
);