Saturate

📁 Source: Aesop/Frontend/Saturate.lean

Statistics

Metric	Count
Definitions runForwardElab, additionalRule, additionalRules, usingRuleSets, addLocalImplications, elabAdditionalForwardRules, elabForwardRule, elabForwardRuleSet, elabForwardRuleSetCore, elabGlobalRuleSets, evalSaturate, evalSaturate?, evalSaturateCore, isImplication, mkForwardOptions, mkHypForwardRule, mkHypImplicationRule?, saturate, saturate?, tacticForward?____, tacticForward____	21
Theorems	0
Total	21

Aesop.ElabM

Definitions

Name	Category	Theorems
runForwardElab 📖	CompOp	—

Aesop.Frontend

Definitions

Name	Category	Theorems
addLocalImplications 📖	CompOp	—
elabAdditionalForwardRules 📖	CompOp	—
elabForwardRule 📖	CompOp	—
elabForwardRuleSet 📖	CompOp	—
elabForwardRuleSetCore 📖	CompOp	—
elabGlobalRuleSets 📖	CompOp	—
evalSaturate 📖	CompOp	—
evalSaturate? 📖	CompOp	—
evalSaturateCore 📖	CompOp	—
isImplication 📖	CompOp	—
mkForwardOptions 📖	CompOp	—
mkHypForwardRule 📖	CompOp	—
mkHypImplicationRule? 📖	CompOp	—
saturate 📖	CompOp	—
saturate? 📖	CompOp	—
tacticForward?____ 📖	CompOp	—
tacticForward____ 📖	CompOp	—

Aesop.Frontend.Parser

Definitions

Name	Category	Theorems
additionalRule 📖	CompOp	—
additionalRules 📖	CompOp	—
usingRuleSets 📖	CompOp	—

---

← Back to Index