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

feat: add replaceFVars

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-22 14:24:03 -07:00
parent bbc1f4d461
commit 0511b73d80
2 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Expr.lean
View file

@ -672,6 +672,10 @@ def replaceFVar (e : Expr) (fvar : Expr) (v : Expr) : Expr :=
def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr :=
replaceFVar e (mkFVar fvarId) v
/-- Replace occurrences of the free variables `fvars` in `e` with `vs` -/
def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr :=
(e.abstract fvars).instantiateRev vs
instance : HasToString Expr :=
⟨Expr.dbgToString⟩

16
tests/lean/run/meta7.lean
View file

@ -137,3 +137,19 @@ check (isDefEq m expected);
pure ()
#eval tst6
def tst7 : MetaM Unit := do
print "----- tst7 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
val ← mkAppM `HasAdd.add #[x, y];
print val;
let val := val.replaceFVars #[x, y] #[mkNatLit 0, mkNatLit 1];
print val;
expected ← mkAppM `HasAdd.add #[mkNatLit 0, mkNatLit 1];
print expected;
check (pure $ val == expected);
pure ()
#eval tst7