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

source ·
pub fn list() -> Term
Expand description

Applied to a Church-encoded number n and n Terms it creates a pair-encoded list of those terms.

LIST ≡ λn.n (λfax.f (CONS x a)) REVERSE NIL ≡ λ 1 (λ λ λ 3 (CONS 1 2)) REVERSE NIL

Example

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

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