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.consumedForwardRuleMatches (r : AddRapp) : Array ForwardRuleMatch

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

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

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

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

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

@[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.