Node IDs #
Equations
Rule Application IDs #
Equations
Iterations #
Equations
Equations
The Tree #
At each point during the search, every node of the tree (goal, rapp or mvar cluster) is in one of these states:
proven
: the node is proven.unprovable
: the node is unprovable, i.e. it will never be proven regardless of any future expansions that might be performed.unknown
: neither of the above.
Every node starts in the unknown
state and may later become either proven
or
unprovable
. After this, the state does not change any more.
Instances For
- notNormal : NormalizationState
- normal (postGoal : Lean.MVarId) (postState : Lean.Meta.SavedState) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormalizationState
- provenByNormalization (postState : Lean.Meta.SavedState) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormalizationState
Instances For
Equations
Instances For
Equations
Instances For
A goal G
can be added to the tree for three reasons:
G
was produced by its parent rule as a subgoal. This is the most common reason.G
was copied because it contains some metavariables which were assigned by its parent rule. In this case, we record goal of whichG
is a copy. We also record the representative of the equivalence class of goals which are copies of each other. E.g. if goal1
is copied to goal2
and goal2
is copied to goal3
, they are all part of the equivalence class with representative1
.
- subgoal : GoalOrigin
- copied («from» rep : GoalId) : GoalOrigin
- droppedMVar : GoalOrigin
Instances For
- id : GoalId
- parent : IO.Ref MVarCluster
- origin : GoalOrigin
- depth : Nat
- state : GoalState
- isIrrelevant : Bool
- isForcedUnprovable : Bool
- preNormGoal : Lean.MVarId
- normalizationState : NormalizationState
- mvars : UnorderedArraySet Lean.MVarId
- forwardState : ForwardState
The forward state reflects the local context of the current goal. Before normalisation, this is the local context of
preNormGoal
; after normalisation, it is the local context of the post-normalisation goal (unless normalisation solved the goal, in which case the forward state is undetermined). - forwardRuleMatches : ForwardRuleMatches
Complete matches of forward rules for the current goal (in the same sense as above).
- successProbability : Percent
- addedInIteration : Iteration
- lastExpandedInIteration : Iteration
- unsafeRulesSelected : Bool
- unsafeQueue : UnsafeQueue
- failedRapps : Array RegularRule
Instances For
Equations
- id : RappId
- parent : IO.Ref Goal
- state : NodeState
- isIrrelevant : Bool
- appliedRule : RegularRule
- scriptSteps? : Option (Array Script.LazyStep)
- originalSubgoals : Array Lean.MVarId
- successProbability : Percent
- metaState : Lean.Meta.SavedState
- introducedMVars : UnorderedArraySet Lean.MVarId
- assignedMVars : UnorderedArraySet Lean.MVarId
Instances For
- mk (d : GoalData RappUnsafe MVarClusterUnsafe) : GoalUnsafe
Instances For
- mk (d : MVarClusterData GoalUnsafe RappUnsafe) : MVarClusterUnsafe
Instances For
- mk (d : RappData GoalUnsafe MVarClusterUnsafe) : RappUnsafe
Instances For
- Goal : Type
- Rapp : Type
- MVarCluster : Type
- introGoal : GoalData self.Rapp self.MVarCluster → self.Goal
- elimGoal : self.Goal → GoalData self.Rapp self.MVarCluster
- introRapp : RappData self.Goal self.MVarCluster → self.Rapp
- elimRapp : self.Rapp → RappData self.Goal self.MVarCluster
- introMVarCluster : MVarClusterData self.Goal self.Rapp → self.MVarCluster
- elimMVarCluster : self.MVarCluster → MVarClusterData self.Goal self.Rapp
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
def
Aesop.MVarCluster.modify
(f : MVarClusterData Goal Rapp → MVarClusterData Goal Rapp)
(c : MVarCluster)
:
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
Miscellaneous Queries #
@[inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Aesop.Rapp.foldSubgoalsM
{m : Type → Type}
{σ : Type}
[Monad m]
[MonadLiftT (ST IO.RealWorld) m]
(init : σ)
(f : σ → GoalRef → m σ)
(r : Rapp)
:
m σ
Equations
Instances For
def
Aesop.Rapp.forSubgoalsM
{m : Type → Type}
[Monad m]
[MonadLiftT (ST IO.RealWorld) m]
(f : GoalRef → m Unit)
(r : Rapp)
:
m Unit