structure Aesop.AddRappextends Aesop.RuleApplication : Type

• goals : Array Subgoal
• postState : Lean.Meta.SavedState
• scriptSteps? : Option (Array Script.LazyStep)
• successProbability? : Option Percent
• parent : GoalRef
• appliedRule : RegularRule
• successProbability : Percent

def Aesop.AddRapp.consumedForwardRuleMatch? (r : AddRapp) : Option ForwardRuleMatch

Equations

• r.consumedForwardRuleMatch? = match r.appliedRule.tac with | Aesop.RuleTacDescr.forwardMatch m => some m | x => none

def Aesop.findPathForAssignedMVars (assignedMVars : UnorderedArraySet Lean.MVarId) (start : GoalRef) : TreeM (Array RappRef × Std.HashSet GoalId)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.getGoalsToCopy (assignedMVars : UnorderedArraySet Lean.MVarId) (start : GoalRef) : TreeM (Array GoalRef)

Equations

• One or more equations did not get rendered due to their size.

unsafe def Aesop.copyGoals (assignedMVars : UnorderedArraySet Lean.MVarId) (start : GoalRef) (parentMetaState : Lean.Meta.SavedState) (parentSuccessProbability : Percent) (depth : Nat) : TreeM (Array Goal)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.makeInitialGoal (goal : Subgoal) (mvars : UnorderedArraySet Lean.MVarId) (parent : MVarClusterRef) (parentMetaState : Lean.Meta.SavedState) (parentForwardState : ForwardState) (parentForwardMatches : ForwardRuleMatches) (consumedForwardRuleMatch? : Option ForwardRuleMatch) (depth : Nat) (successProbability : Percent) (origin : GoalOrigin) : TreeM Goal

Equations

• One or more equations did not get rendered due to their size.

unsafe def Aesop.addRappUnsafe (r : AddRapp) : TreeM RappRef

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by Aesop.addRappUnsafe]

opaque Aesop.addRapp : AddRapp → TreeM RappRef

Adds a new rapp and its subgoals. If the rapp assigns mvars, all relevant goals containing these mvars are copied as children of the rapp as well. If the rapp drops mvars, these are treated as assigned mvars, in the sense that the same goals are copied as if the dropped mvar had been assigned.

Note that adding a rapp may prove the parent goal, but this function does not make the necessary changes. So after calling it, you should check whether the rapp's parent goal is proven and mark it accordingly.