Match
📁 Source: Aesop/Forward/Match.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsreconstructArgs, toMessageData, anyHyp, apply, foldHyps, foldHypsM, getProof, getPropHyps, instToMessageData, Match, addHypOrPatSubst, containsHyp, containsPatSubst, initial, elabForwardRuleTerm, forwardRuleMatchesToNormRules?, forwardRuleMatchesToSafeRules?, forwardRuleMatchesToUnsafeRules? | 18 |
| Theorems | 0 |
| Total | 18 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
Match 📖 | CompData | — |
elabForwardRuleTerm 📖 | CompOp | — |
forwardRuleMatchesToNormRules? 📖 | CompOp | — |
forwardRuleMatchesToSafeRules? 📖 | CompOp | — |
forwardRuleMatchesToUnsafeRules? 📖 | CompOp | — |
Aesop.CompleteMatch
Definitions
| Name | Category | Theorems |
|---|---|---|
reconstructArgs 📖 | CompOp | — |
toMessageData 📖 | CompOp | — |
Aesop.ForwardRuleMatch
Definitions
| Name | Category | Theorems |
|---|---|---|
anyHyp 📖 | CompOp | — |
apply 📖 | CompOp | — |
foldHyps 📖 | CompOp | — |
foldHypsM 📖 | CompOp | — |
getProof 📖 | CompOp | — |
getPropHyps 📖 | CompOp | — |
instToMessageData 📖 | CompOp | — |
Aesop.Match
Definitions
| Name | Category | Theorems |
|---|---|---|
addHypOrPatSubst 📖 | CompOp | — |
containsHyp 📖 | CompOp | — |
containsPatSubst 📖 | CompOp | — |
initial 📖 | CompOp | — |
---