From b83691baa278f4b3311f2ca10dbf1d02fd2e1b95 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 27 Feb 2020 10:56:29 -0800
Subject: [PATCH] feat: compute `fvarSubst`

---
 src/Init/Lean/Meta/Tactic/FVarSubst.lean | 2 ++
 src/Init/Lean/Meta/Tactic/Subst.lean     | 7 ++++++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/Tactic/FVarSubst.lean b/src/Init/Lean/Meta/Tactic/FVarSubst.lean
index b7d636023d..cc349eca1e 100644
--- a/src/Init/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Init/Lean/Meta/Tactic/FVarSubst.lean
@@ -20,6 +20,8 @@ structure FVarSubst :=
 
 namespace FVarSubst
 
+def empty : FVarSubst := {}
+
 def insert (s : FVarSubst) (fvarId : FVarId) (e : Expr) : FVarSubst :=
 { map := s.map.insert fvarId e }
 
diff --git a/src/Init/Lean/Meta/Tactic/Subst.lean b/src/Init/Lean/Meta/Tactic/Subst.lean
index bd3cc3090f..3572732d44 100644
--- a/src/Init/Lean/Meta/Tactic/Subst.lean
+++ b/src/Init/Lean/Meta/Tactic/Subst.lean
@@ -57,7 +57,12 @@ withMVarContext mvarId $ do
             mvarId ← clear mvarId hFVarId;
             mvarId ← clear mvarId aFVarId;
             (newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false;
-            fvarSubst ← pure {FVarSubst . }; -- TODO
+            fvarSubst ← newFVars.size.foldM
+              (fun i (fvarSubst : FVarSubst) =>
+                let var      := vars.get! i;
+                let newFVar := newFVars.get! i;
+                pure $ fvarSubst.insert var (mkFVar newFVar))
+              FVarSubst.empty;
             pure (fvarSubst, mvarId)
           };
           if depElim then do