Basic
📁 Source: Aesop/RuleTac/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsCasesPattern, CasesTarget, RuleApplication, check, goals, postState, scriptSteps?, successProbability?, ofSingleRuleTac, ofTacticSyntax, RuleTacInput, goal, indexMatchLocations, mvars, options, patternSubsts?, RuleTacOutput, applications, SingleRuleTac, toRuleTac, Subgoal, diff, mvarId, instInhabitedCasesPattern, instInhabitedCasesTarget, default, instInhabitedRuleTac, instInhabitedRuleTacInput, default, instInhabitedRuleTacOutput, default, instInhabitedSubgoal, default, mvarIdToSubgoal | 34 |
| Theorems | 0 |
| Total | 34 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
CasesPattern 📖 | CompOp | — |
CasesTarget 📖 | CompData | — |
RuleApplication 📖 | CompData | — |
RuleTacInput 📖 | CompData | — |
RuleTacOutput 📖 | CompData | — |
SingleRuleTac 📖 | CompOp | — |
Subgoal 📖 | CompData | — |
instInhabitedCasesPattern 📖 | CompOp | — |
instInhabitedCasesTarget 📖 | CompOp | — |
instInhabitedRuleTac 📖 | CompOp | — |
instInhabitedRuleTacInput 📖 | CompOp | — |
instInhabitedRuleTacOutput 📖 | CompOp | — |
instInhabitedSubgoal 📖 | CompOp | — |
mvarIdToSubgoal 📖 | CompOp | — |
Aesop.RuleApplication
Definitions
| Name | Category | Theorems |
|---|---|---|
check 📖 | CompOp | — |
goals 📖 | CompOp | — |
postState 📖 | CompOp | — |
scriptSteps? 📖 | CompOp | — |
successProbability? 📖 | CompOp | — |
Aesop.RuleTac
Definitions
| Name | Category | Theorems |
|---|---|---|
ofSingleRuleTac 📖 | CompOp | — |
ofTacticSyntax 📖 | CompOp | — |
Aesop.RuleTacInput
Definitions
| Name | Category | Theorems |
|---|---|---|
goal 📖 | CompOp | — |
indexMatchLocations 📖 | CompOp | — |
mvars 📖 | CompOp | — |
options 📖 | CompOp | — |
patternSubsts? 📖 | CompOp | — |
Aesop.RuleTacOutput
Definitions
| Name | Category | Theorems |
|---|---|---|
applications 📖 | CompOp | — |
Aesop.SingleRuleTac
Definitions
| Name | Category | Theorems |
|---|---|---|
toRuleTac 📖 | CompOp | — |
Aesop.Subgoal
Definitions
| Name | Category | Theorems |
|---|---|---|
diff 📖 | CompOp | — |
mvarId 📖 | CompOp | — |
Aesop.instInhabitedCasesTarget
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedRuleTacInput
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedRuleTacOutput
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedSubgoal
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---