From a2f24fac65e779fbc7db37f29a9f00195bd8de1a Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 7 Aug 2025 08:23:01 -0700 Subject: [PATCH] chore: use `unreachable!` for unreachable cases, not silent fallback (#9790) --- src/Lean/Compiler/IR/RC.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 9b4ac05fac..c4ff5c6a54 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -288,7 +288,7 @@ partial def visitFnBody (b : FnBody) (ctx : Context) : FnBody × LiveVarSet := let bLiveVars := collectLiveVars b ctx.jpLiveVarMap ⟨b, bLiveVars⟩ | .unreachable => ⟨.unreachable, {}⟩ - | _ => ⟨b, {}⟩ -- unreachable if well-formed + | .set .. | .setTag .. | .inc .. | .dec .. | .del .. => unreachable! partial def visitDecl (env : Environment) (decls : Array Decl) (d : Decl) : Decl := match d with