From 8f40899cde2eb5fed6d78ad6b9b4a6846f5a9725 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Oct 2022 09:58:47 -0700 Subject: [PATCH] feat: add `Expr.updateFVar!` --- src/Lean/Expr.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index e493535eeb..629348f10c 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -1470,6 +1470,11 @@ def updateApp! (e : Expr) (newFn : Expr) (newArg : Expr) : Expr := | app _ _ => mkApp newFn newArg | _ => panic! "application expected" +@[inline] def updateFVar! (e : Expr) (fvarIdNew : FVarId) : Expr := + match e with + | .fvar fvarId => if fvarId == fvarIdNew then e else .fvar fvarIdNew + | _ => panic! "fvar expected" + @[inline] private unsafe def updateConst!Impl (e : Expr) (newLevels : List Level) : Expr := match e with | const n ls => if ptrEqList ls newLevels then e else mkConst n newLevels