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

pub fn reverse() -> Term

Reverses a pair-encoded list.

REVERSE ≡ Z (λzal.IS_NIL l (λx.a) (λx.z (CONS (HEAD l) a) (TAIL l) I)) NIL ≡ Z (λ λ λ IS_NIL 1 (λ 3) (λ 4 (CONS (HEAD 2) 3) (TAIL 2)) I) NIL

Example

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

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

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