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

fix: make sure borrow annotations do not affect auto-completion

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-09 13:47:28 -07:00
parent bc8daee635
commit 3318c75bed
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Server/Completion.lean
View file

@ -180,7 +180,8 @@ private def isDotCompletionMethod (info : ConstantInfo) : MetaM Bool :=
forallTelescopeReducing info.type fun xs _ => do
for x in xs do
let localDecl ← getLocalDecl x.fvarId!
if localDecl.type.getAppFn.isConstOf info.name.getPrefix then
let type := localDecl.type.consumeMData
if type.getAppFn.isConstOf info.name.getPrefix then
return true
return false