max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Expr.updateFVar!

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-28 09:58:47 -07:00
parent 6d46829599
commit 8f40899cde
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Expr.lean
View file

@ -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