Function lambda_calculus::reduction::beta_once
[−]
[src]
pub fn beta_once(term: Term) -> Term
Performs a single normal-order β-reduction on self
.
Example
use lambda_calculus::arithmetic::succ; use lambda_calculus::reduction::beta_once; // SUCC := λ λ λ 2 (3 2 1), ONE := λ λ 2 1 let succ_one = succ().app(1.into()); assert_eq!(&*format!("{}", beta_once(succ_one)), "λλ2((λλ21)21)");