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.
leanprover · Jan 18, 2025 · 5e63dd2 · 5e63dd2
1 parent 98e3d6f
commit 5e63dd2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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