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

fix: dotted notation corner case

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-01 18:20:36 -07:00
parent cfb4e306f7
commit be014b1fc9
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/Elab/App.lean
View file

@ -866,9 +866,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
let some expectedType := expectedType?
| throwError "invalid dotted identifier notation, expected type must be known"
forallTelescopeReducing expectedType fun _ resultType => do
let resultTypeFn := (← instantiateMVars resultType).getAppFn
let resultTypeFn := (← instantiateMVars resultType).consumeMData.getAppFn
tryPostponeIfMVar resultTypeFn
let .const declName .. := resultTypeFn
let .const declName .. := resultTypeFn.consumeMData
| throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
let idNew := declName ++ id.getId.eraseMacroScopes
unless (← getEnv).contains idNew do