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