From 31e05cd2bd3b9a895ababfebddacfd82b40efd43 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Tue, 5 Aug 2025 17:49:49 -0700 Subject: [PATCH] chore: fix typos (#9747) --- src/Lean/Compiler/IR/RC.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 20710ec7d0..efa0b7ee6b 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -107,13 +107,13 @@ private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : let info := getVarInfo ctx x if !info.type.isPossibleRef || !isFirstOcc xs i then b else - let numConsuptions := getNumConsumptions x xs consumeParamPred -- number of times the argument is + let numConsumptions := getNumConsumptions x xs consumeParamPred let numIncs := if !info.mustBeConsumed || liveVarsAfter.contains x || -- `x` is live after executing instruction isBorrowParamAux x xs consumeParamPred -- `x` is used in a position that is passed as a borrow reference - then numConsuptions - else numConsuptions - 1 + then numConsumptions + else numConsumptions - 1 addInc ctx x b numIncs private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=