Function lambda_calculus::list::reverse

pub fn reverse() -> Term

Reverses a Church list.

REVERSE := Z (λzal.NULL l (λx.a) (λx.z (PAIR (FST l) a) (SND l) I)) NIL = Z (λ λ λ NULL 1 (λ 3) (λ 4 (PAIR (FST 2) 3) (SND 2)) I) NIL

Example

use lambda_calculus::term::Term;
use lambda_calculus::list::reverse;
use lambda_calculus::arithmetic::{zero, one};
use lambda_calculus::reduction::beta;
use lambda_calculus::reduction::Order::*;

let list = Term::from(vec![one(), one(), zero()]);

assert_eq!(beta(app!(reverse(), list), NOR, 0),
           Term::from(vec![zero(), one(), one()])
);