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-09 16:42:41 -07:00
parent 20bc004c70
commit 02fc447b04
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/Meta/Check.lean
View file

@ -19,7 +19,7 @@ _ ← getLevel e; pure ()
def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
lctx ← getLCtx;
match lctx.find? fvarId with
| some (LocalDecl.ldecl _ n t v b _) => do
| some (LocalDecl.ldecl _ _ n t v _) => do
vType ← inferType v;
throwError $
"invalid let declaration, term" ++ indentExpr v