Function lambda_calculus::combinators::I

source ·

pub fn I() -> Term

Expand description

I - the identity combinator.

I ≡ λx.x ≡ λ 1

Example

use lambda_calculus::combinators::I;
use lambda_calculus::*;

assert_eq!(beta(app(I(), Var(1)), NOR, 0), Var(1));
assert_eq!(beta(app(I(), abs(Var(1))), NOR, 0), abs(Var(1)));