Tactic
📁 Source: Aesop/Frontend/Tactic.lean
Statistics
| Metric | Count |
|---|---|
Definitionsquot, aesopTactic, aesopTactic?, ruleSetSpec, «tactic_clause(Add_)»»), «tactic_clause(Config:=_)»»), «tactic_clause(Erase_)»»), «tactic_clause(Rule_sets:=[_])»»), «tactic_clause(Simp_config:=_)»»), additionalRules, enabledRuleSets, erasedRules, getRuleSet, options, parse, simpConfig, simpConfigSyntax?, updateRuleSet, elabConfigUnsafe, elabOptions, elabSimpConfig, elabSimpConfigCtx, tactic_clause | 23 |
| Theorems | 0 |
| Total | 23 |
Aesop.Frontend
Definitions
| Name | Category | Theorems |
|---|---|---|
elabConfigUnsafe 📖 | CompOp | — |
elabOptions 📖 | CompOp | — |
elabSimpConfig 📖 | CompOp | — |
elabSimpConfigCtx 📖 | CompOp | — |
Aesop.Frontend.Parser
Definitions
| Name | Category | Theorems |
|---|---|---|
aesopTactic 📖 | CompOp | — |
aesopTactic? 📖 | CompOp | — |
ruleSetSpec 📖 | CompOp | — |
«tactic_clause(Add_)» 📖» "API Documentation") | CompOp | — |
«tactic_clause(Config:=_)» 📖» "API Documentation") | CompOp | — |
«tactic_clause(Erase_)» 📖» "API Documentation") | CompOp | — |
«tactic_clause(Rule_sets:=[_])» 📖» "API Documentation") | CompOp | — |
«tactic_clause(Simp_config:=_)» 📖» "API Documentation") | CompOp | — |
Aesop.Frontend.Parser.Aesop.tactic_clause
Definitions
| Name | Category | Theorems |
|---|---|---|
quot 📖 | CompOp | — |
Aesop.Frontend.TacticConfig
Definitions
| Name | Category | Theorems |
|---|---|---|
additionalRules 📖 | CompOp | — |
enabledRuleSets 📖 | CompOp | — |
erasedRules 📖 | CompOp | — |
getRuleSet 📖 | CompOp | — |
options 📖 | CompOp | — |
parse 📖 | CompOp | — |
simpConfig 📖 | CompOp | — |
simpConfigSyntax? 📖 | CompOp | — |
updateRuleSet 📖 | CompOp | — |
Lean.Parser.Category.Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
tactic_clause 📖 | CompOp | — |
---