Function lambda_calculus::data::list::pair::init

pub fn init() -> Term

Applied to a pair-encoded list it returns the list without the last element.

INIT ≡ Z (λzl.IS_NIL l (λx.NIL) (λx.IS_NIL (TAIL l) NIL (CONS (HEAD l) (z (TAIL l)))) I) ≡ Z (λ λ IS_NIL 1 (λ NIL) (λ IS_NIL (TAIL 2) NIL (CONS (HEAD 2) (3 (TAIL 2)))) I)

Example

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

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

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