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

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-17 13:50:05 -07:00
parent 8142548237
commit 4ea8db2722
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Meta/Tactic/Target.lean
View file

@ -14,8 +14,8 @@ namespace Meta
/--
Convert the given goal `Ctx |- target` into `Ctx |- targetNew` using an equality proof `eqProof : target = targetNew`.
It assumes `eqProof` has type `target = targetNew` -/
def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId := do
withMVarContext mvarId $ do
def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId :=
withMVarContext mvarId do
checkNotAssigned mvarId `replaceTarget;
tag ← getMVarTag mvarId;
newMVar ← mkFreshExprSyntheticOpaqueMVar targetNew tag;
@ -35,7 +35,7 @@ withMVarContext mvarId $ do
```
to create a checkpoint. -/
def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
withMVarContext mvarId $ do
withMVarContext mvarId do
checkNotAssigned mvarId `change;
target ← getMVarType mvarId;
if target == targetNew then pure mvarId
@ -47,7 +47,7 @@ withMVarContext mvarId $ do
pure newMVar.mvarId!
def change (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
withMVarContext mvarId $ do
withMVarContext mvarId do
target ← getMVarType mvarId;
unlessM (isDefEq target targetNew) $
throwTacticEx `change mvarId