TacticState

📁 Source: Aesop/Script/TacticState.lean

Statistics

Metric	Count
Definitions TacticState, applyTactic, eraseSolvedGoals, focus, getMainGoal?, getVisibleGoalIndex, getVisibleGoalIndex?, invisibleGoals, mkInitial, onGoalM, solveVisibleGoals, visibleGoals, visibleGoalsHaveMVars, instInhabitedTacticState, default	15
Theorems	0
Total	15

Aesop.Script

Definitions

Name	Category	Theorems
TacticState 📖	CompData	—
instInhabitedTacticState 📖	CompOp	—

Aesop.Script.TacticState

Definitions

Name	Category	Theorems
applyTactic 📖	CompOp	—
eraseSolvedGoals 📖	CompOp	—
focus 📖	CompOp	—
getMainGoal? 📖	CompOp	—
getVisibleGoalIndex 📖	CompOp	—
getVisibleGoalIndex? 📖	CompOp	—
invisibleGoals 📖	CompOp	—
mkInitial 📖	CompOp	—
onGoalM 📖	CompOp	—
solveVisibleGoals 📖	CompOp	—
visibleGoals 📖	CompOp	—
visibleGoalsHaveMVars 📖	CompOp	—

Aesop.Script.instInhabitedTacticState

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index