Forward

📁 Source: Aesop/RuleTac/Forward.lean

Statistics

Metric	Count
Definitions ForwardM, Context, forwardHypData, maxDepth?, toAssert, usedHyps, instInhabitedContext, default, instInhabitedState, default, applyForwardRule, assertForwardHyp, forward, forwardConst, forwardExpr, forwardMatch, forwardMatches, forwardTerm, makeForwardHypProofs, makeForwardHypProofs'	20
Theorems	0
Total	20

Aesop.RuleTac

Definitions

Name	Category	Theorems
ForwardM 📖	CompOp	—
applyForwardRule 📖	CompOp	—
assertForwardHyp 📖	CompOp	—
forward 📖	CompOp	—
forwardConst 📖	CompOp	—
forwardExpr 📖	CompOp	—
forwardMatch 📖	CompOp	—
forwardMatches 📖	CompOp	—
forwardTerm 📖	CompOp	—
makeForwardHypProofs 📖	CompOp	—
makeForwardHypProofs' 📖	CompOp	—

Aesop.RuleTac.ForwardM

Definitions

Name	Category	Theorems
Context 📖	CompData	—
instInhabitedContext 📖	CompOp	—
instInhabitedState 📖	CompOp	—

Aesop.RuleTac.ForwardM.Context

Definitions

Name	Category	Theorems
forwardHypData 📖	CompOp	—
maxDepth? 📖	CompOp	—

Aesop.RuleTac.ForwardM.State

Definitions

Name	Category	Theorems
toAssert 📖	CompOp	—
usedHyps 📖	CompOp	—

Aesop.RuleTac.ForwardM.instInhabitedContext

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.RuleTac.ForwardM.instInhabitedState

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index