Function lamcal::reduce

pub fn reduce<B>(expr: &Term) -> Term where
    B: BetaReduce, 

Performs a β-reduction on a given lambda expression applying the given reduction strategy.

The reduction strategy to be used must be given as the type parameter B, like in the example below.

This function returns the result as a new Term. The given Term remains unchanged. If you want to apply a β-reduction modifying the term in place use the associated function Term::reduce instead.

Examples

let expr = app![
    lam("a", var("a")),
    lam("b", lam("c", var("b"))),
    var("x"),
    lam("e", var("f"))
];

let reduced = reduce::<NormalOrder<Enumerate>>(&expr);

assert_eq!(reduced, var("x"));