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

chore: upstream MVarId.applyConst (#3362)

Browse source 
Helper function for applying a constant to the goal, with fresh universe
metavariables.
This commit is contained in:
Scott Morrison 2024-02-16 13:08:47 +11:00 • committed by GitHub
parent eaf44d74ae
commit 229f16f421
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Tactic/Apply.lean
View file

@ -188,6 +188,10 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
mvarId.apply e cfg
/-- Short-hand for applying a constant to the goal. -/
def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
mvar.apply (← mkConstWithFreshMVarLevels c) cfg
partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) :=
mvarId.withContext do
mvarId.checkNotAssigned `splitAnd