chore: comment

2021-04-13 10:34:19 -07:00 · 2021-04-13 10:34:19 -07:00 · 1a2a089c28
commit 1a2a089c28
parent adda3a9e02
1 changed files with 3 additions and 1 deletions
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@ -388,7 +388,9 @@ private def shouldBetaReduce (e : Expr) (recFnName : Name) : Bool :=
  This is useful to improve the effectiveness of `elimRecursion`.
  Example:
  ```
-
+  def f : Nat → Nat
+    | 0 => 1
+    | i+1 => (fun x => f x) i
  ```
 -/
 private def preprocess (e : Expr) (recFnName : Name) : CoreM Expr :=