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