RuleTerm

📁 Source: Aesop/RuleTac/RuleTerm.lean

Statistics

Metric	Count
Definitions expr, instToMessageData, name, ofElaboratedTerm, scope, toRuleTerm, RuleTerm, instInhabitedElabRuleTerm, default, instInhabitedRuleTerm, default, instToMessageDataRuleTerm	12
Theorems	0
Total	12

Aesop

Definitions

Name	Category	Theorems
RuleTerm 📖	CompData	—
instInhabitedElabRuleTerm 📖	CompOp	—
instInhabitedRuleTerm 📖	CompOp	—
instToMessageDataRuleTerm 📖	CompOp	—

Aesop.ElabRuleTerm

Definitions

Name	Category	Theorems
expr 📖	CompOp	—
instToMessageData 📖	CompOp	—
name 📖	CompOp	—
ofElaboratedTerm 📖	CompOp	—
scope 📖	CompOp	—
toRuleTerm 📖	CompOp	—

Aesop.instInhabitedElabRuleTerm

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedRuleTerm

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index