- visibleGoals : Array GoalWithMVars
- invisibleGoals : Std.HashSet Lean.MVarId
Instances For
Equations
Instances For
Equations
Instances For
def
Aesop.Script.TacticState.getVisibleGoalIndex
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(ts : TacticState)
(goal : Lean.MVarId)
:
m Nat
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Aesop.Script.TacticState.eraseSolvedGoals
(ts : TacticState)
(preMCtx postMCtx : Lean.MetavarContext)
:
Equations
Instances For
def
Aesop.Script.TacticState.eraseSolvedGoals.mvarWasSolved
(preMCtx postMCtx : Lean.MetavarContext)
(mvarId : Lean.MVarId)
:
Equations
Instances For
def
Aesop.Script.TacticState.applyTactic
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(ts : TacticState)
(inGoal : Lean.MVarId)
(outGoals : Array GoalWithMVars)
(preMCtx postMCtx : Lean.MetavarContext)
:
Equations
Instances For
def
Aesop.Script.TacticState.focus
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
(ts : TacticState)
(goal : Lean.MVarId)
:
Equations
Instances For
@[always_inline]
def
Aesop.Script.TacticState.onGoalM
{m : Type → Type}
[Monad m]
[Lean.MonadError m]
{α : Type}
(ts : TacticState)
(g : Lean.MVarId)
(f : TacticState → m (α × TacticState))
:
m (α × TacticState)