diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 7e821da44e..e876165c84 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -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