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

feat: add subst?

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-18 14:26:14 -08:00
parent c12fa6f0e2
commit c816524d8d
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/Tactic/Subst.lean
View file

@ -165,8 +165,11 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
| throwTacticEx `subst mvarId m!"did not find equation for eliminating '{mkFVar hFVarId}'"
return (← substCore mvarId fvarId (symm := symm) (tryToSkip := true)).2
def subst? (mvarId : MVarId) (hFVarId : FVarId) : MetaM (Option MVarId) :=
observing? (subst mvarId hFVarId)
def trySubst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId := do
match (← observing? (subst mvarId hFVarId)) with
match (← subst? mvarId hFVarId) with
| some mvarId => return mvarId
| none => return mvarId