State

📁 Source: Aesop/Tree/State.lean

Statistics

Metric	Count
Definitions State, State, State, isIrrelevantNoCache, isProvenByNormalizationNoCache, isProvenByRuleApplicationNoCache, isProvenNoCache, isUnprovableNoCache, stateNoCache, checkAndMarkUnprovable, markForcedUnprovable, markProvenByNormalization, markSubtreeIrrelevant, markUnprovable, isIrrelevantNoCache, isProvenNoCache, isUnprovableNoCache, stateNoCache, markSubtreeIrrelevant, State, isIrrelevantNoCache, isProvenNoCache, isUnprovableNoCache, stateNoCache, markProven, markSubtreeIrrelevant, State, State, State, State, State, State, markSubtreeIrrelevant	33
Theorems	0
Total	33

Aesop.BaseM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.EqualUpToIdsM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.ExtractScriptM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.Goal

Definitions

Name	Category	Theorems
isIrrelevantNoCache 📖	CompOp	—
isProvenByNormalizationNoCache 📖	CompOp	—
isProvenByRuleApplicationNoCache 📖	CompOp	—
isProvenNoCache 📖	CompOp	—
isUnprovableNoCache 📖	CompOp	—
stateNoCache 📖	CompOp	—

Aesop.GoalRef

Definitions

Name	Category	Theorems
checkAndMarkUnprovable 📖	CompOp	—
markForcedUnprovable 📖	CompOp	—
markProvenByNormalization 📖	CompOp	—
markSubtreeIrrelevant 📖	CompOp	—
markUnprovable 📖	CompOp	—

Aesop.MVarCluster

Definitions

Name	Category	Theorems
isIrrelevantNoCache 📖	CompOp	—
isProvenNoCache 📖	CompOp	—
isUnprovableNoCache 📖	CompOp	—
stateNoCache 📖	CompOp	—

Aesop.MVarClusterRef

Definitions

Name	Category	Theorems
markSubtreeIrrelevant 📖	CompOp	—

Aesop.NormM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.Rapp

Definitions

Name	Category	Theorems
isIrrelevantNoCache 📖	CompOp	—
isProvenNoCache 📖	CompOp	—
isUnprovableNoCache 📖	CompOp	—
stateNoCache 📖	CompOp	—

Aesop.RappRef

Definitions

Name	Category	Theorems
markProven 📖	CompOp	—
markSubtreeIrrelevant 📖	CompOp	—

Aesop.RuleTac.ForwardM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.SafeExpansionM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.Script.DynStructureM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.Script.StaticStructureM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.SearchM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.TreeM

Definitions

Name	Category	Theorems
State 📖	CompData	—

Aesop.TreeRef

Definitions

Name	Category	Theorems
markSubtreeIrrelevant 📖	CompOp	—

---

← Back to Index