Norm
📁 Source: Aesop/Search/Expansion/Norm.lean
Statistics
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
NormM 📖 | CompOp | — |
NormRuleResult 📖 | CompData | — |
NormSeqResult 📖 | CompData | — |
NormStep 📖 | CompOp | — |
applyDiffToForwardState 📖 | CompOp | — |
checkSimp 📖 | CompOp | — |
eraseForwardRuleMatch 📖 | CompOp | — |
getForwardState 📖 | CompOp | — |
getResetForwardState 📖 | CompOp | — |
mkNormSimpScriptStep 📖 | CompOp | — |
modifyForwardState 📖 | CompOp | — |
normSimp 📖 | CompOp | — |
normSimpCore 📖 | CompOp | — |
normUnfold 📖 | CompOp | — |
normUnfoldCore 📖 | CompOp | — |
normalizeGoalIfNecessary 📖 | CompOp | — |
normalizeGoalMVar 📖 | CompOp | — |
optNormRuleResultEmoji 📖 | CompOp | — |
optNormRuleResultToNormSeqResult 📖 | CompOp | — |
runFirstNormRule 📖 | CompOp | — |
runNormRule 📖 | CompOp | — |
runNormRuleTac 📖 | CompOp | — |
runNormSteps 📖 | CompOp | — |
updateForwardState 📖 | CompOp | — |
withNormTraceNode 📖 | CompOp | — |
Aesop.NormM
Definitions
| Name | Category | Theorems |
|---|---|---|
Context 📖 | CompData | — |
instInhabitedState 📖 | CompOp | — |
Aesop.NormM.Context
Definitions
| Name | Category | Theorems |
|---|---|---|
normSimpContext 📖 | CompOp | — |
options 📖 | CompOp | — |
ruleSet 📖 | CompOp | — |
Aesop.NormM.State
Definitions
| Name | Category | Theorems |
|---|---|---|
forwardRuleMatches 📖 | CompOp | — |
forwardState 📖 | CompOp | — |
Aesop.NormM.instInhabitedState
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.NormRuleResult
Definitions
| Name | Category | Theorems |
|---|---|---|
newGoal? 📖 | CompOp | — |
steps? 📖 | CompOp | — |
toNormSeqResult 📖 | CompOp | — |
Aesop.NormStep
Definitions
| Name | Category | Theorems |
|---|---|---|
runPostSimpRules 📖 | CompOp | — |
runPreSimpRules 📖 | CompOp | — |
simp 📖 | CompOp | — |
unfold 📖 | CompOp | — |
---