structure Aesop.Script.TacticState : Type

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

Instances For

• Aesop.Script.instInhabitedTacticState

instance Aesop.Script.instInhabitedTacticState : Inhabited Aesop.Script.TacticState

Equations

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

def Aesop.Script.TacticState.mkInitial (goal : Lean.MVarId) : Lean.MetaM Aesop.Script.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 : Aesop.Script.TacticState) (goal : Lean.MVarId) : Option Nat

Equations

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

def Aesop.Script.TacticState.getVisibleGoalIndex {m : Type → Type} [Monad m] [Lean.MonadError m] (ts : Aesop.Script.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 : Aesop.Script.TacticState) : Option Lean.MVarId

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.Script.TacticState.eraseSolvedGoals.mvarWasSolved (preMCtx : Lean.MetavarContext) (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 : Aesop.Script.TacticState) (inGoal : Lean.MVarId) (outGoals : Array Aesop.GoalWithMVars) (preMCtx : Lean.MetavarContext) (postMCtx : Lean.MetavarContext) : m Aesop.Script.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 : Aesop.Script.TacticState) (goal : Lean.MVarId) : m Aesop.Script.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 : Aesop.Script.TacticState) (g : Lean.MVarId) (f : Aesop.Script.TacticState → m (α × Aesop.Script.TacticState)) : m (α × Aesop.Script.TacticState)

Equations

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