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

chore: better error message for loose bvar in whnf

Browse source
This commit is contained in:
Jannis Limperg 2023-07-19 13:44:20 +02:00 • committed by Leonardo de Moura
parent 367b38701f
commit 6407197e54
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/WHNF.lean
View file

@ -314,7 +314,7 @@ end
| .lam .. => return e
| .sort .. => return e
| .lit .. => return e
| .bvar .. => unreachable!
| .bvar .. => panic! "loose bvar in expression"
| .letE .. => k e
| .const .. => k e
| .app .. => k e