Function lambda_calculus::list::list

pub fn list() -> Term

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

LIST := λn.n (λfax.f (PAIR x a)) REVERSE NIL = λ 1 (λ λ λ 3 (PAIR 1 2)) REVERSE NIL

Example

use lambda_calculus::term::Term;
use lambda_calculus::list::list;
use lambda_calculus::reduction::beta;
use lambda_calculus::reduction::Order::*;

assert_eq!(beta(app!(list(), 3.into(), 0.into(), 1.into(), 1.into()), NOR, 0),
           Term::from(vec![0.into(), 1.into(), 1.into()]));