max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix typo in docstring of mkMVar (#6687)

Browse source 
This PR fixes a very small typo in the docstring of `mkMVar` that
misspelled the function it recommends to use instead.
This commit is contained in:
Andrés Goens 2025-01-18 13:28:33 +01:00 • committed by GitHub
parent 98e3d6f663
commit 5e63dd292f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Expr.lean
View file

@ -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