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

fix: error message

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-11 07:32:30 -07:00
parent 6cf652606a
commit 2978d7af32
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/Elab/App.lean
View file

@ -344,7 +344,7 @@ match eType.getAppFn, lval with
match findMethod? env structName fieldName with
| some (baseStructName, fullName) => pure $ LValResolution.const baseStructName structName fullName
| none => throwLValError e eType $
"invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ (structName ++ fieldName) ++ "'"
"invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ (structName ++ fieldName : Name) ++ "'"
};
-- search local context first, then environment
let searchCtx : Unit → TermElabM LValResolution := fun _ => do {