fix: Bindings in prograde tactics #90
|
@ -247,7 +247,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
|
|||
-- See Lean.Elab.Tactic.Conv.convTarget
|
||||
let convMVar ← Elab.Tactic.withMainContext do
|
||||
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
|
||||
Elab.Tactic.setGoals [newGoal.mvarId!]
|
||||
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
|
||||
pure rhs.mvarId!
|
||||
return (← MonadBacktrack.saveState, convMVar)
|
||||
try
|
||||
|
|
|
@ -25,7 +25,7 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
|||
(tagSuffix := .anonymous )
|
||||
(allowNaturalHoles := true)
|
||||
goal.assign expr
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -31,7 +31,7 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
|||
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruenceArg goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
|
||||
|
@ -60,7 +60,7 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
|||
def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruenceFun goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
|
||||
|
@ -93,6 +93,6 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
|||
def evalCongruence: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruence goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -100,6 +100,6 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
|
|||
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
||||
Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
|
||||
Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -17,6 +17,6 @@ def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
|
|||
let goal ← Elab.Tactic.getMainGoal
|
||||
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
|
||||
noConfuse goal h
|
||||
Elab.Tactic.setGoals []
|
||||
Elab.Tactic.replaceMainGoal []
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
Loading…
Reference in New Issue