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

chore: Improve LCNF check goto error message

Browse source
This commit is contained in:
Henrik Böving 2022-10-20 00:12:26 +02:00 • committed by Leonardo de Moura
parent fc304d95c0
commit a608532fd4
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/Compiler/LCNF/Check.lean
View file

@ -238,7 +238,7 @@ partial def check (code : Code) : CheckM Unit := do
checkJpInScope fvarId
let decl ← getFunDecl fvarId
unless decl.getArity == args.size do
throwError "invalid LCNF `jmp`, join point has #{decl.getArity} parameters, but #{args.size} were provided"
throwError "invalid LCNF `goto`, join point {decl.binderName} has #{decl.getArity} parameters, but #{args.size} were provided"
checkAppArgs (.fvar fvarId) args
| .return fvarId => checkFVar fvarId
| .unreach .. => pure ()