From 6d236fbf2e6b4c9d7be20acaef2cd4cd1ad42287 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Mar 2021 07:13:32 -0800
Subject: [PATCH] chore: fix docstring

---
 src/Lean/Meta/ExprDefEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 117581b680..780e60a812 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -107,7 +107,7 @@ def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
   ```
   fun x₁ ... xₙ => ?m x₁ ... xₙ =?= t
   t =?= fun x₁ ... xₙ => ?m x₁ ... xₙ
-
+  ```
   This is important because type inference often produces
   eta-expanded terms, and without this extra case, we could
   introduce counter intuitive behavior.