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

feat: compute fvarSubst

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-27 10:56:29 -08:00
parent 6a19f54344
commit b83691baa2
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Meta/Tactic/FVarSubst.lean
View file

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

7
src/Init/Lean/Meta/Tactic/Subst.lean
View file

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