Function lambda_calculus::list::length

pub fn length() -> Term

Applied to a Church-encoded list it returns its Church-encoded length.

LENGTH := Y (λgcx.NULL x c (g (SUCC c) (SECOND x))) ZERO = Y (λλλ NULL 1 2 (3 (SUCC 2) (SECOND 1))) ZERO

Example

use lambda_calculus::term::Term;
use lambda_calculus::list::{length, nil};
use lambda_calculus::reduction::beta_full;

let list_4 = Term::from(vec![1.into(), 1.into(), 0.into(), 1.into()]);

assert_eq!(beta_full(length().app(nil())),  0.into());
assert_eq!(beta_full(length().app(list_4)), 4.into());