State

📁 Source: Aesop/Forward/State.lean

Statistics

Metric	Count
Definitions ClusterState, AddM, Context, premiseLMVars, premiseMVars, run, addHyp, addMatch, addQueuedRawHyps, addRawHyp, completeMatches, conclusionDeps, enqueueRawHyp, eraseEnqueuedRawHyp, eraseHyp, erasePatSubst, findSlot?, haveHypForEachSlot, instInhabited, instToMessageData, matchPremise?, slot!, slotQueues, slots, stats, update, variableMap, initialRuleState, ForwardState, enqueueHyp, enqueueHypWithPatSubsts, enqueuePatSubst, enqueuePatSubsts, enqueueTargetPatSubsts, eraseHyp, erasePatSubsts, eraseTargetPatSubsts, hyps, instEmptyCollection, instToMessageData, patSubsts, ruleStates, stats, update, Hyp, containsHyp, fvarId?, instBEq, instHashable, isPatSubst, subst, InstMap, eraseHyp, erasePatSubst, find?, findD, insertHyp, insertMatch, insertMatchCore, instEmptyCollection, instToMessageData, map, modify, modifyMapsForSlotsFrom, stats, PatSubstSource, RawHyp, RuleState, clusterStates, enqueueRawHyp, eraseHyp, erasePatSubst, patSubstSources, rule, stats, update, VariableMap, addHyp, addMatch, eraseHyp, erasePatSubst, find, find?, findHyps, findMatches, instEmptyCollection, instToMessageData, map, modify, modifyM, stats, instBEqPatSubstSource, beq, instBEqRawHyp, beq, instHashablePatSubstSource, hash, instHashableRawHyp, hash, instInhabitedForwardState, default, instInhabitedHyp, default, instInhabitedInstMap, default, instInhabitedPatSubstSource, default, instInhabitedRawHyp, default, instInhabitedRuleState, default, instInhabitedVariableMap, default, instToMessageDataRawHyp, instToMessageDataRuleState	115
Theorems slotQueues_size	1
Total	116

Aesop

Definitions

Name	Category	Theorems
ClusterState 📖	CompData	—
ForwardState 📖	CompData	—
Hyp 📖	CompData	—
InstMap 📖	CompData	—
PatSubstSource 📖	CompData	—
RawHyp 📖	CompData	1 math math: ClusterState.slotQueues_size
RuleState 📖	CompData	—
VariableMap 📖	CompData	—
instBEqPatSubstSource 📖	CompOp	—
instBEqRawHyp 📖	CompOp	—
instHashablePatSubstSource 📖	CompOp	—
instHashableRawHyp 📖	CompOp	—
instInhabitedForwardState 📖	CompOp	—
instInhabitedHyp 📖	CompOp	—
instInhabitedInstMap 📖	CompOp	—
instInhabitedPatSubstSource 📖	CompOp	—
instInhabitedRawHyp 📖	CompOp	—
instInhabitedRuleState 📖	CompOp	—
instInhabitedVariableMap 📖	CompOp	—
instToMessageDataRawHyp 📖	CompOp	—
instToMessageDataRuleState 📖	CompOp	—

Aesop.ClusterState

Definitions

Name	Category	Theorems
AddM 📖	CompOp	—
addHyp 📖	CompOp	—
addMatch 📖	CompOp	—
addQueuedRawHyps 📖	CompOp	—
addRawHyp 📖	CompOp	—
completeMatches 📖	CompOp	—
conclusionDeps 📖	CompOp	—
enqueueRawHyp 📖	CompOp	—
eraseEnqueuedRawHyp 📖	CompOp	—
eraseHyp 📖	CompOp	—
erasePatSubst 📖	CompOp	—
findSlot? 📖	CompOp	—
haveHypForEachSlot 📖	CompOp	—
instInhabited 📖	CompOp	—
instToMessageData 📖	CompOp	—
matchPremise? 📖	CompOp	—
slot! 📖	CompOp	—
slotQueues 📖	CompOp	1 math math: slotQueues_size
slots 📖	CompOp	1 math math: slotQueues_size
stats 📖	CompOp	—
update 📖	CompOp	—
variableMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slotQueues_size 📖	mathematical	—	Aesop.RawHyp slotQueues Aesop.Slot slots	—	—

Aesop.ClusterState.AddM

Definitions

Name	Category	Theorems
Context 📖	CompData	—
run 📖	CompOp	—

Aesop.ClusterState.AddM.Context

Definitions

Name	Category	Theorems
premiseLMVars 📖	CompOp	—
premiseMVars 📖	CompOp	—

Aesop.ForwardRule

Definitions

Name	Category	Theorems
initialRuleState 📖	CompOp	—

Aesop.ForwardState

Definitions

Name	Category	Theorems
enqueueHyp 📖	CompOp	—
enqueueHypWithPatSubsts 📖	CompOp	—
enqueuePatSubst 📖	CompOp	—
enqueuePatSubsts 📖	CompOp	—
enqueueTargetPatSubsts 📖	CompOp	—
eraseHyp 📖	CompOp	—
erasePatSubsts 📖	CompOp	—
eraseTargetPatSubsts 📖	CompOp	—
hyps 📖	CompOp	—
instEmptyCollection 📖	CompOp	—
instToMessageData 📖	CompOp	—
patSubsts 📖	CompOp	—
ruleStates 📖	CompOp	—
stats 📖	CompOp	—
update 📖	CompOp	—

Aesop.Hyp

Definitions

Name	Category	Theorems
containsHyp 📖	CompOp	—
fvarId? 📖	CompOp	—
instBEq 📖	CompOp	—
instHashable 📖	CompOp	—
isPatSubst 📖	CompOp	—
subst 📖	CompOp	—

Aesop.InstMap

Definitions

Name	Category	Theorems
eraseHyp 📖	CompOp	—
erasePatSubst 📖	CompOp	—
find? 📖	CompOp	—
findD 📖	CompOp	—
insertHyp 📖	CompOp	—
insertMatch 📖	CompOp	—
insertMatchCore 📖	CompOp	—
instEmptyCollection 📖	CompOp	—
instToMessageData 📖	CompOp	—
map 📖	CompOp	—
modify 📖	CompOp	—
modifyMapsForSlotsFrom 📖	CompOp	—
stats 📖	CompOp	—

Aesop.RuleState

Definitions

Name	Category	Theorems
clusterStates 📖	CompOp	—
enqueueRawHyp 📖	CompOp	—
eraseHyp 📖	CompOp	—
erasePatSubst 📖	CompOp	—
patSubstSources 📖	CompOp	—
rule 📖	CompOp	—
stats 📖	CompOp	—
update 📖	CompOp	—

Aesop.VariableMap

Definitions

Name	Category	Theorems
addHyp 📖	CompOp	—
addMatch 📖	CompOp	—
eraseHyp 📖	CompOp	—
erasePatSubst 📖	CompOp	—
find 📖	CompOp	—
find? 📖	CompOp	—
findHyps 📖	CompOp	—
findMatches 📖	CompOp	—
instEmptyCollection 📖	CompOp	—
instToMessageData 📖	CompOp	—
map 📖	CompOp	—
modify 📖	CompOp	—
modifyM 📖	CompOp	—
stats 📖	CompOp	—

Aesop.instBEqPatSubstSource

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Aesop.instBEqRawHyp

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Aesop.instHashablePatSubstSource

Definitions

Name	Category	Theorems
hash 📖	CompOp	—

Aesop.instHashableRawHyp

Definitions

Name	Category	Theorems
hash 📖	CompOp	—

Aesop.instInhabitedForwardState

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedHyp

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedInstMap

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedPatSubstSource

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedRawHyp

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedRuleState

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instInhabitedVariableMap

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index