TreeM
📁 Source: Aesop/Tree/TreeM.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsallIntroducedMVars, nextGoalId, nextRappId, numGoals, numRapps, root, rootMetaState, TreeM, Context, currentIteration, ruleSet, tree, instInhabited, instMonad, instMonadStateOfTree, run', getAllIntroducedMVars, getAndIncrementNextGoalId, getAndIncrementNextRappId, getRootGoal, getRootMVarCluster, getRootMVarId, getRootMetaState, incrementNumGoals, incrementNumRapps, mkInitialTree | 26 |
| Theorems | 0 |
| Total | 26 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
TreeM 📖 | CompOp | — |
getAllIntroducedMVars 📖 | CompOp | — |
getAndIncrementNextGoalId 📖 | CompOp | — |
getAndIncrementNextRappId 📖 | CompOp | — |
getRootGoal 📖 | CompOp | — |
getRootMVarCluster 📖 | CompOp | — |
getRootMVarId 📖 | CompOp | — |
getRootMetaState 📖 | CompOp | — |
incrementNumGoals 📖 | CompOp | — |
incrementNumRapps 📖 | CompOp | — |
mkInitialTree 📖 | CompOp | — |
Aesop.Tree
Definitions
| Name | Category | Theorems |
|---|---|---|
allIntroducedMVars 📖 | CompOp | — |
nextGoalId 📖 | CompOp | — |
nextRappId 📖 | CompOp | — |
numGoals 📖 | CompOp | — |
numRapps 📖 | CompOp | — |
root 📖 | CompOp | — |
rootMetaState 📖 | CompOp | — |
Aesop.TreeM
Definitions
| Name | Category | Theorems |
|---|---|---|
Context 📖 | CompData | — |
instInhabited 📖 | CompOp | — |
instMonad 📖 | CompOp | — |
instMonadStateOfTree 📖 | CompOp | — |
run' 📖 | CompOp | — |
Aesop.TreeM.Context
Definitions
| Name | Category | Theorems |
|---|---|---|
currentIteration 📖 | CompOp | — |
ruleSet 📖 | CompOp | — |
Aesop.TreeM.State
Definitions
| Name | Category | Theorems |
|---|---|---|
tree 📖 | CompOp | — |
---