Function lambda_calculus::list::reverse

pub fn reverse() -> Term

Reverses a Church-encoded list.

REVERSE := Y (λgal.NULL l a (g (PAIR (FIRST l) a) (SECOND l))) NIL = Y (λ λ λ NULL 1 2 (3 (PAIR (FIRST 1) 2) (SECOND 1))) NIL

Example

use lambda_calculus::term::Term;
use lambda_calculus::list::reverse;
use lambda_calculus::arithmetic::{zero, one};
use lambda_calculus::reduction::beta_full;

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

assert_eq!(beta_full(reverse().app(list)), Term::from(vec![zero(), one(), one()]));