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

doc: clarify mkLocalDecl

Browse source
This commit is contained in:
E.W.Ayers 2022-03-24 16:41:26 -04:00 • committed by Leonardo de Moura
parent 6f5fc72c06
commit 1e69639fd2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/LocalContext.lean
View file

@ -129,8 +129,8 @@ def isEmpty (lctx : LocalContext) : Bool :=
/-- Low level API for creating local declarations.
It is used to implement actions in the monads `Elab` and `Tactic`.
It should not be used directly since the argument `(name : Name)` is
assumed to be "unique". -/
It should not be used directly since the argument `(fvarId : FVarId)` is
assumed to be unique. You can create a unique fvarId with `mkFreshFVarId`. -/
@[export lean_local_ctx_mk_local_decl]
def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalContext :=
match lctx with