RuleSet

📁 Source: Aesop/RuleSet.lean

Statistics

Metric	Count
Definitions BaseRuleSet, add, contains, empty, erase, erased, forwardRuleNames, forwardRules, merge, normRules, ruleNames, rulePatterns, safeRules, trace, unfoldRules, unsafeRules, GlobalRuleSet, contains, empty, erase, modifyBase, modifyBaseM, onBase, onBaseM, simpTheorems, simprocs, toBaseRuleSet, trace, add, applicableForwardRules, applicableForwardRulesWith, applicableNormalizationRules, applicableNormalizationRulesWith, applicableSafeRules, applicableSafeRulesWith, applicableUnsafeRules, applicableUnsafeRulesWith, constForwardRuleMatches, contains, containsGlobalSimpTheorem, empty, erase, forwardRulePatternSubstsInExpr, forwardRulePatternSubstsInLocalDecl, localNormSimpRules, modifyBase, modifyBaseM, onBase, onBaseM, simpTheoremsArray, simprocsArray, toBaseRuleSet, trace, unindex, instEmptyCollectionBaseRuleSet, instEmptyCollectionGlobalRuleSet, instEmptyCollectionLocalRuleSet, instInhabitedBaseRuleSet, default, instInhabitedGlobalRuleSet, default, instInhabitedLocalRuleSet, mkLocalRuleSet, unindexPredicate?	64
Theorems simpTheoremsArrayNonempty, simprocsArrayNonempty	2
Total	66

Aesop

Definitions

Name	Category	Theorems
BaseRuleSet 📖	CompData	—
GlobalRuleSet 📖	CompData	—
instEmptyCollectionBaseRuleSet 📖	CompOp	—
instEmptyCollectionGlobalRuleSet 📖	CompOp	—
instEmptyCollectionLocalRuleSet 📖	CompOp	—
instInhabitedBaseRuleSet 📖	CompOp	—
instInhabitedGlobalRuleSet 📖	CompOp	—
instInhabitedLocalRuleSet 📖	CompOp	—
mkLocalRuleSet 📖	CompOp	—
unindexPredicate? 📖	CompOp	—

Aesop.BaseRuleSet

Definitions

Name	Category	Theorems
add 📖	CompOp	—
contains 📖	CompOp	—
empty 📖	CompOp	—
erase 📖	CompOp	—
erased 📖	CompOp	—
forwardRuleNames 📖	CompOp	—
forwardRules 📖	CompOp	—
merge 📖	CompOp	—
normRules 📖	CompOp	—
ruleNames 📖	CompOp	—
rulePatterns 📖	CompOp	—
safeRules 📖	CompOp	—
trace 📖	CompOp	—
unfoldRules 📖	CompOp	—
unsafeRules 📖	CompOp	—

Aesop.GlobalRuleSet

Definitions

Name	Category	Theorems
contains 📖	CompOp	—
empty 📖	CompOp	—
erase 📖	CompOp	—
modifyBase 📖	CompOp	—
modifyBaseM 📖	CompOp	—
onBase 📖	CompOp	—
onBaseM 📖	CompOp	—
simpTheorems 📖	CompOp	—
simprocs 📖	CompOp	—
toBaseRuleSet 📖	CompOp	—
trace 📖	CompOp	—

Aesop.LocalRuleSet

Definitions

Name	Category	Theorems
add 📖	CompOp	—
applicableForwardRules 📖	CompOp	—
applicableForwardRulesWith 📖	CompOp	—
applicableNormalizationRules 📖	CompOp	—
applicableNormalizationRulesWith 📖	CompOp	—
applicableSafeRules 📖	CompOp	—
applicableSafeRulesWith 📖	CompOp	—
applicableUnsafeRules 📖	CompOp	—
applicableUnsafeRulesWith 📖	CompOp	—
constForwardRuleMatches 📖	CompOp	—
contains 📖	CompOp	—
containsGlobalSimpTheorem 📖	CompOp	—
empty 📖	CompOp	—
erase 📖	CompOp	—
forwardRulePatternSubstsInExpr 📖	CompOp	—
forwardRulePatternSubstsInLocalDecl 📖	CompOp	—
localNormSimpRules 📖	CompOp	—
modifyBase 📖	CompOp	—
modifyBaseM 📖	CompOp	—
onBase 📖	CompOp	—
onBaseM 📖	CompOp	—
simpTheoremsArray 📖	CompOp	1 math math: simpTheoremsArrayNonempty
simprocsArray 📖	CompOp	1 math math: simprocsArrayNonempty
toBaseRuleSet 📖	CompOp	—
trace 📖	CompOp	—
unindex 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
simpTheoremsArrayNonempty 📖	mathematical	—	simpTheoremsArray	—	—
simprocsArrayNonempty 📖	mathematical	—	simprocsArray	—	—

Aesop.instInhabitedBaseRuleSet

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedGlobalRuleSet

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index