Core
📁 Source: Mathlib/Tactic/Core.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsallGoals, andThenOnSubgoals, filterOutImplementationDetails, getFVarIdAt, getFVarIdsAt, iterateAtMost, iterateExactly', iterateRange, iterateUntilFailure, iterateUntilFailureCount, iterateUntilFailureWithResults, introsWithBinderIdents, setProtected, toModifiers, toPreDefinition, getDSimpArgs, getSimpArgs, getUsingArg, getWithArgs, tacticRepeat1_, usingArg, withArgs, getMathlibDir, getPackageDir | 24 |
| Theorems | 0 |
| Total | 24 |
Lean
Definitions
| Name | Category | Theorems |
|---|---|---|
setProtected 📖 | CompOp | — |
toModifiers 📖 | CompOp | — |
toPreDefinition 📖 | CompOp | — |
Lean.Elab.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
allGoals 📖 | CompOp | — |
andThenOnSubgoals 📖 | CompOp | — |
filterOutImplementationDetails 📖 | CompOp | — |
getFVarIdAt 📖 | CompOp | — |
getFVarIdsAt 📖 | CompOp | — |
iterateAtMost 📖 | CompOp | — |
iterateExactly' 📖 | CompOp | — |
iterateRange 📖 | CompOp | — |
iterateUntilFailure 📖 | CompOp | — |
iterateUntilFailureCount 📖 | CompOp | — |
iterateUntilFailureWithResults 📖 | CompOp | — |
Lean.MVarId
Definitions
| Name | Category | Theorems |
|---|---|---|
introsWithBinderIdents 📖 | CompOp | — |
Mathlib
Definitions
| Name | Category | Theorems |
|---|---|---|
getMathlibDir 📖 | CompOp | — |
getPackageDir 📖 | CompOp | — |
Mathlib.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
getDSimpArgs 📖 | CompOp | — |
getSimpArgs 📖 | CompOp | — |
getUsingArg 📖 | CompOp | — |
getWithArgs 📖 | CompOp | — |
tacticRepeat1_ 📖 | CompOp | — |
usingArg 📖 | CompOp | — |
withArgs 📖 | CompOp | — |
---