Function lambda_calculus::data::list::parigot::tail

pub fn tail() -> Term

Applied to a Parigot-encoded list it returns a new list with all its elements but the first one.

TAIL ≡ λl.l UD (λhtx.t) ≡ λ 1 UD (λ λ λ 2)

Example

use lambda_calculus::data::list::parigot::tail;
use lambda_calculus::*;

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

assert_eq!(
    beta(app(tail(), list), NOR, 0),
    vec![2, 3].into_parigot()
);