structure Aesop.Script.TacticState : Type

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

instance Aesop.Script.instInhabitedTacticState : Inhabited TacticState

Equations

• Aesop.Script.instInhabitedTacticState = { default := { visibleGoals := default, invisibleGoals := default } }

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

Equations

• Aesop.Script.TacticState.mkInitial goal = do let __do_lift ← goal.getMVarDependencies pure { visibleGoals := #[{ goal := goal, mvars := __do_lift }], invisibleGoals := ∅ }

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

Equations

• ts.getVisibleGoalIndex? goal = Array.findIdx? (fun (x : Aesop.GoalWithMVars) => x.goal == goal) ts.visibleGoals

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ts.getMainGoal? = Option.map (fun (x : Aesop.GoalWithMVars) => x.goal) ts.visibleGoals[0]?

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

Equations

• ts.visibleGoalsHaveMVars = ts.visibleGoals.any fun (g : Aesop.GoalWithMVars) => !g.mvars.isEmpty

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

Equations

• ts.solveVisibleGoals = { visibleGoals := #[], invisibleGoals := ts.invisibleGoals }

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Script.TacticState.eraseSolvedGoals.mvarWasSolved (preMCtx postMCtx : Lean.MetavarContext) (mvarId : Lean.MVarId) : Bool

Equations

• Aesop.Script.TacticState.eraseSolvedGoals.mvarWasSolved preMCtx postMCtx mvarId = (postMCtx.isExprMVarAssignedOrDelayedAssigned mvarId && !preMCtx.isExprMVarAssignedOrDelayedAssigned mvarId)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.