RuleInfo

📁 Source: Aesop/Forward/RuleInfo.lean

Statistics

Metric	Count
Definitions ForwardRuleInfo, conclusionDeps, isConstant, numLevelParams, numPremises, ofExpr, rulePatternInfo?, slotClusters, Slot, common, deps, forwardDeps, index, premiseIndex, typeDiscrTreeKeys?, instBEqSlot, instHashableSlot, instInhabitedForwardRuleInfo, default, instInhabitedSlot, default	21
Theorems	0
Total	21

Aesop

Definitions

Name	Category	Theorems
ForwardRuleInfo 📖	CompData	—
Slot 📖	CompData	1 math math: ClusterState.slotQueues_size
instBEqSlot 📖	CompOp	—
instHashableSlot 📖	CompOp	—
instInhabitedForwardRuleInfo 📖	CompOp	—
instInhabitedSlot 📖	CompOp	—

Aesop.ForwardRuleInfo

Definitions

Name	Category	Theorems
conclusionDeps 📖	CompOp	—
isConstant 📖	CompOp	—
numLevelParams 📖	CompOp	—
numPremises 📖	CompOp	—
ofExpr 📖	CompOp	—
rulePatternInfo? 📖	CompOp	—
slotClusters 📖	CompOp	—

Aesop.Slot

Definitions

Name	Category	Theorems
common 📖	CompOp	—
deps 📖	CompOp	—
forwardDeps 📖	CompOp	—
index 📖	CompOp	—
premiseIndex 📖	CompOp	—
typeDiscrTreeKeys? 📖	CompOp	—

Aesop.instInhabitedForwardRuleInfo

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedSlot

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index