Function lambda_calculus::pair::second

pub fn second() -> Term

Applied to a Church-encoded pair (a, b) it yields b.

SECOND := λp.p FALSE = λ 1 FALSE

Example

use lambda_calculus::pair::{pair, second};
use lambda_calculus::arithmetic::{zero, one};
use lambda_calculus::reduction::beta_full;

let pair_0_1 = pair().app(zero()).app(one());

assert_eq!(beta_full(second().app(pair_0_1)), one());