From 98e9fc20d5f8a00fb1d9f1f32fce1914ed826548 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jul 2020 13:06:45 -0700 Subject: [PATCH] feat: add `replaceFVar` --- src/Lean/Expr.lean | 6 ++++++ src/Lean/Meta/Tactic/Subst.lean | 8 ++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index d8420da3d9..49ec3aa07b 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -635,6 +635,12 @@ constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := arbitrary _ @[extern "lean_expr_abstract_range"] constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := arbitrary _ +def replaceFVar (e : Expr) (fvar : Expr) (v : Expr) : Expr := +(e.abstract #[fvar]).instantiate1 v + +def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr := +replaceFVar e (mkFVar fvarId) v + instance : HasToString Expr := ⟨Expr.dbgToString⟩ diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index 5919d7650f..1b96253852 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -66,9 +66,9 @@ withMVarContext mvarId $ do pure (fvarSubst, mvarId) }; if depElim then do - let newType := (type.abstract #[a]).instantiate1 b; + let newType := type.replaceFVar a b; reflB ← mkEqRefl b; - let newType := (newType.abstract #[h]).instantiate1 reflB; + let newType := newType.replaceFVar h reflB; if symm then do motive ← mkLambda #[a, h] type; continue motive newType @@ -82,13 +82,13 @@ withMVarContext mvarId $ do motive ← withLocalDecl `_h hAuxType BinderInfo.default $ fun hAux => do { hAuxSymm ← mkEqSymm hAux; /- replace h in type with hAuxSymm -/ - let newType := (type.abstract #[h]).instantiate1 hAuxSymm; + let newType := type.replaceFVar h hAuxSymm; mkLambda #[a, hAux] newType }; continue motive newType else do motive ← mkLambda #[a] type; - let newType := (type.abstract #[a]).instantiate1 b; + let newType := type.replaceFVar a b; continue motive newType | _ => throwTacticEx `subst mvarId $