ElabRuleTerm
📁 Source: Aesop/RuleTac/ElabRuleTerm.lean
Statistics
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
ElabRuleTerm 📖 | CompData | — |
checkElabRuleTermForSimp 📖 | CompOp | — |
elabGlobalRuleIdent? 📖 | CompOp | — |
elabInductiveRuleIdent? 📖 | CompOp | — |
elabRuleTermForApplyLike 📖 | CompOp | — |
elabRuleTermForApplyLikeCore 📖 | CompOp | — |
elabRuleTermForApplyLikeMetaM 📖 | CompOp | — |
elabRuleTermForSimpCore 📖 | CompOp | — |
elabRuleTermForSimpMetaM 📖 | CompOp | — |
elabSimpTheorems 📖 | CompOp | — |
matchInductiveTypeSynonym? 📖 | CompOp | — |
mkSimpArgs 📖 | CompOp | — |
runTacticMAsElabM 📖 | CompOp | — |
runTacticMAsTermElabM 📖 | CompOp | — |
withFullElaboration 📖 | CompOp | — |
---