Function lambda_calculus::data::list::parigot::head

source ·

pub fn head() -> Term

Expand description

Applied to a Parigot-encoded list it returns its first element.

HEAD ≡ λl.l UD (λhtx.h) ≡ λ 1 UD (λ λ λ 3)

Example

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

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

assert_eq!(
    beta(app(head(), list), NOR, 0),
    1.into_parigot()
);