structure Aesop.Script.TacticState : Type

• visibleGoals : Array GoalWithMVars
• invisibleGoals : Std.HashSet Lean.MVarId

@[implicit_reducible]

instance Aesop.Script.instInhabitedTacticState : Inhabited TacticState

def Aesop.Script.instInhabitedTacticState.default : TacticState

def Aesop.Script.TacticState.mkInitial (goal : Lean.MVarId) : Lean.MetaM TacticState

def Aesop.Script.TacticState.getVisibleGoalIndex? (ts : TacticState) (goal : Lean.MVarId) : Option Nat

def Aesop.Script.TacticState.getVisibleGoalIndex {m : Type → Type} [Monad m] [Lean.MonadError m] (ts : TacticState) (goal : Lean.MVarId) : m Nat

def Aesop.Script.TacticState.getMainGoal? (ts : TacticState) : Option Lean.MVarId

def Aesop.Script.TacticState.visibleGoalsHaveMVars (ts : TacticState) : Bool

def Aesop.Script.TacticState.solveVisibleGoals (ts : TacticState) : TacticState

def Aesop.Script.TacticState.eraseSolvedGoals (ts : TacticState) (preMCtx postMCtx : Lean.MetavarContext) : TacticState

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) : m TacticState

def Aesop.Script.TacticState.focus {m : Type → Type} [Monad m] [Lean.MonadError m] (ts : TacticState) (goal : Lean.MVarId) : m TacticState

@[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)