From 1a2a089c2843db03aa38775599c0896e2cc2b362 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Apr 2021 10:34:19 -0700
Subject: [PATCH] chore: comment

---
 src/Lean/Elab/PreDefinition/Structural.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index b6d8f15a44..ec56bf6a64 100644
--- 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 :=