From 6407197e540d509bb201601b47a3e15c43faefab Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Wed, 19 Jul 2023 13:44:20 +0200
Subject: [PATCH] chore: better error message for loose bvar in whnf

---
 src/Lean/Meta/WHNF.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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