Documentation Verification Report

Substitution

📁 Source: Aesop/Forward/Substitution.lean

Statistics

MetricCount
DefinitionsSubstitution, containsHyp, empty, find?, findLevel?, insert, insertLevel, instBEq, instHashable, instOrd, instToMessageData, levels, mergeCompatible, openRuleType, premises, specializeRule, instInhabitedSubstitution, default, openRuleType
19
Theorems0
Total19

Aesop

Definitions

NameCategoryTheorems
Substitution 📖CompData
instInhabitedSubstitution 📖CompOp
openRuleType 📖CompOp

Aesop.Substitution

Definitions

NameCategoryTheorems
containsHyp 📖CompOp
empty 📖CompOp
find? 📖CompOp
findLevel? 📖CompOp
insert 📖CompOp
insertLevel 📖CompOp
instBEq 📖CompOp
instHashable 📖CompOp
instOrd 📖CompOp
instToMessageData 📖CompOp
levels 📖CompOp
mergeCompatible 📖CompOp
openRuleType 📖CompOp
premises 📖CompOp
specializeRule 📖CompOp

Aesop.instInhabitedSubstitution

Definitions

NameCategoryTheorems
default 📖CompOp

---

← Back to Index