Function lambda_calculus::reduction::beta_once

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)");