TacticAnalysis
📁 Source: Mathlib/Tactic/TacticAnalysis.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsComplexConfig, ctx, out, tell, test, trigger, Config, ofComplex, run, Entry, declName, import, optionName, Pass, opt, toConfig, TacticNode, ctxI, mayFail, runTacticCode, runTacticCodeCapturingInfoTree, tacI, TriggerCondition, findTacticSeqs, instBEqTriggerCondition, beq, instOrdEntry, runPass, runPasses, tacticAnalysis, tacticAnalysisExt, testTacticSeq, tacticAnalysis, dummy | 34 |
| Theorems | 0 |
| Total | 34 |
Mathlib.TacticAnalysis
Definitions
| Name | Category | Theorems |
|---|---|---|
ComplexConfig 📖 | CompData | — |
Config 📖 | CompData | — |
Entry 📖 | CompData | — |
Pass 📖 | CompData | — |
TacticNode 📖 | CompData | — |
TriggerCondition 📖 | CompData | — |
findTacticSeqs 📖 | CompOp | — |
instBEqTriggerCondition 📖 | CompOp | — |
instOrdEntry 📖 | CompOp | — |
runPass 📖 | CompOp | — |
runPasses 📖 | CompOp | — |
tacticAnalysis 📖 | CompOp | — |
tacticAnalysisExt 📖 | CompOp | — |
testTacticSeq 📖 | CompOp | — |
Mathlib.TacticAnalysis.ComplexConfig
Definitions
| Name | Category | Theorems |
|---|---|---|
ctx 📖 | CompOp | — |
out 📖 | CompOp | — |
tell 📖 | CompOp | — |
test 📖 | CompOp | — |
trigger 📖 | CompOp | — |
Mathlib.TacticAnalysis.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
ofComplex 📖 | CompOp | — |
run 📖 | CompOp | — |
Mathlib.TacticAnalysis.Entry
Definitions
| Name | Category | Theorems |
|---|---|---|
declName 📖 | CompOp | — |
import 📖 | CompOp | — |
optionName 📖 | CompOp | — |
Mathlib.TacticAnalysis.Pass
Definitions
| Name | Category | Theorems |
|---|---|---|
opt 📖 | CompOp | — |
toConfig 📖 | CompOp | — |
Mathlib.TacticAnalysis.TacticNode
Definitions
| Name | Category | Theorems |
|---|---|---|
ctxI 📖 | CompOp | — |
mayFail 📖 | CompOp | — |
runTacticCode 📖 | CompOp | — |
runTacticCodeCapturingInfoTree 📖 | CompOp | — |
tacI 📖 | CompOp | — |
Mathlib.TacticAnalysis.instBEqTriggerCondition
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
linter
Definitions
| Name | Category | Theorems |
|---|---|---|
tacticAnalysis 📖 | CompOp | — |
linter.tacticAnalysis
Definitions
| Name | Category | Theorems |
|---|---|---|
dummy 📖 | CompOp | — |
---