Step
📁 Source: Aesop/Script/Step.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsLazyStep, BuildInput, postGoals, tac, tacticBuilder, build, erasePostStateAssignments, postGoals, postState, preGoal, preState, runFirstSuccessfulTacticBuilder, tacticBuilders, toStep, Step, instToMessageData, mkSorry, postGoals, postState, preGoal, preState, render, sTactic?, tactic, uTactic, validate, applyStep, mkOnGoal, mkOneBasedNumLit | 29 |
TheoremstacticBuilders_ne | 1 |
| Total | 30 |
Aesop.Script
Definitions
| Name | Category | Theorems |
|---|---|---|
LazyStep 📖 | CompData | — |
Step 📖 | CompData | — |
mkOnGoal 📖 | CompOp | — |
mkOneBasedNumLit 📖 | CompOp | — |
Aesop.Script.LazyStep
Definitions
| Name | Category | Theorems |
|---|---|---|
BuildInput 📖 | CompData | — |
build 📖 | CompOp | — |
erasePostStateAssignments 📖 | CompOp | — |
postGoals 📖 | CompOp | — |
postState 📖 | CompOp | — |
preGoal 📖 | CompOp | — |
preState 📖 | CompOp | — |
runFirstSuccessfulTacticBuilder 📖 | CompOp | — |
tacticBuilders 📖 | CompOp | |
toStep 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
tacticBuilders_ne 📖 | mathematical | — | Aesop.Script.TacticBuildertacticBuilders | — | — |
Aesop.Script.LazyStep.BuildInput
Definitions
| Name | Category | Theorems |
|---|---|---|
postGoals 📖 | CompOp | — |
tac 📖 | CompOp | — |
tacticBuilder 📖 | CompOp | — |
Aesop.Script.Step
Definitions
| Name | Category | Theorems |
|---|---|---|
instToMessageData 📖 | CompOp | — |
mkSorry 📖 | CompOp | — |
postGoals 📖 | CompOp | — |
postState 📖 | CompOp | — |
preGoal 📖 | CompOp | — |
preState 📖 | CompOp | — |
render 📖 | CompOp | — |
sTactic? 📖 | CompOp | — |
tactic 📖 | CompOp | — |
uTactic 📖 | CompOp | — |
validate 📖 | CompOp | — |
Aesop.Script.TacticState
Definitions
| Name | Category | Theorems |
|---|---|---|
applyStep 📖 | CompOp | — |
---