Preprocesses the expressions to improve the effectiveness of wfRecursion
.
Unlike Lean.Elab.Structural.preprocess
, do not beta-reduce, as it could
remove let_fun
-lambdas that contain explicit termination proofs.
Preprocesses the expressions to improve the effectiveness of wfRecursion
.
Unlike Lean.Elab.Structural.preprocess
, do not beta-reduce, as it could
remove let_fun
-lambdas that contain explicit termination proofs.