Beta reduce terms where the recursive function occurs in the lambda term.
This is useful to improve the effectiveness of elimRecursion.
Example:
def f : Nat → Nat
| 0 => 1
| i+1 => (fun x => f x) i
Equations
- One or more equations did not get rendered due to their size.