From 5e63dd292f53fad4b4355c702a9ee277424ec6fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Sat, 18 Jan 2025 13:28:33 +0100
Subject: [PATCH] chore: fix typo in docstring of mkMVar (#6687)

This PR fixes a very small typo in the docstring of `mkMVar` that
misspelled the function it recommends to use instead.
---
 src/Lean/Expr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index f60754e41f..53f43b58c4 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -639,7 +639,7 @@ def mkFVar (fvarId : FVarId) : Expr :=
 /--
 `.mvar mvarId` is now the preferred form.
 This function is seldom used, metavariables are often created using functions such
-as `mkFresheExprMVar` at `MetaM`.
+as `mkFreshExprMVar` at `MetaM`.
 -/
 def mkMVar (mvarId : MVarId) : Expr :=
   .mvar mvarId