From 2104fd7da90ce810ea66949634f68c4cc1a08484 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 7 Aug 2025 09:27:23 -0700 Subject: [PATCH] chore: remove unused default (#9791) --- 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 c4ff5c6a54..ead58e93e7 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -45,7 +45,7 @@ def getJPParams (ctx : Context) (j : JoinPointId) : Array Param := ctx.localCtx.getJPParams j |>.get! def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet := - ctx.jpLiveVarMap.get? j |>.getD {} + ctx.jpLiveVarMap.get! j def mustConsume (ctx : Context) (x : VarId) : Bool := let info := getVarInfo ctx x