SpecificTactics
📁 Source: Aesop/Script/SpecificTactics.lean
Statistics
| Metric | Count |
|---|---|
Definitionsskip, apply, applyStx, assertHypothesis, cases, casesOrObtain, clear, exactFVar, extN, intros, obtain, renameInaccessibleFVars, replace, simpAllOrSimpAtStar, simpAllOrSimpAtStarOnly, splitAt, splitTarget, substFVars, substFVars', unfold, unfoldAt, applyS, assertHypothesisS, clearS, introsS, introsUnfoldingS, renameInaccessibleFVarsS, replaceFVarS, splitFirstHypothesisS?, splitTargetS?, straightLineExtS, tryCasesS, tryClearManyS, tryClearS, tryExactFVarS, unfoldManyAtS, unfoldManyStarS, unfoldManyTargetS | 38 |
| Theorems | 0 |
| Total | 38 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
applyS 📖 | CompOp | — |
assertHypothesisS 📖 | CompOp | — |
clearS 📖 | CompOp | — |
introsS 📖 | CompOp | — |
introsUnfoldingS 📖 | CompOp | — |
renameInaccessibleFVarsS 📖 | CompOp | — |
replaceFVarS 📖 | CompOp | — |
splitFirstHypothesisS? 📖 | CompOp | — |
splitTargetS? 📖 | CompOp | — |
straightLineExtS 📖 | CompOp | — |
tryCasesS 📖 | CompOp | — |
tryClearManyS 📖 | CompOp | — |
tryClearS 📖 | CompOp | — |
tryExactFVarS 📖 | CompOp | — |
unfoldManyAtS 📖 | CompOp | — |
unfoldManyStarS 📖 | CompOp | — |
unfoldManyTargetS 📖 | CompOp | — |
Aesop.Script.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
skip 📖 | CompOp | — |
Aesop.Script.TacticBuilder
Definitions
| Name | Category | Theorems |
|---|---|---|
apply 📖 | CompOp | — |
applyStx 📖 | CompOp | — |
assertHypothesis 📖 | CompOp | — |
cases 📖 | CompOp | — |
casesOrObtain 📖 | CompOp | — |
clear 📖 | CompOp | — |
exactFVar 📖 | CompOp | — |
extN 📖 | CompOp | — |
intros 📖 | CompOp | — |
obtain 📖 | CompOp | — |
renameInaccessibleFVars 📖 | CompOp | — |
replace 📖 | CompOp | — |
simpAllOrSimpAtStar 📖 | CompOp | — |
simpAllOrSimpAtStarOnly 📖 | CompOp | — |
splitAt 📖 | CompOp | — |
splitTarget 📖 | CompOp | — |
substFVars 📖 | CompOp | — |
substFVars' 📖 | CompOp | — |
unfold 📖 | CompOp | — |
unfoldAt 📖 | CompOp | — |
---