structure Aesop.AddRappextends Aesop.RuleApplication : Type

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

@[implemented_by _private.Aesop.Tree.AddRapp.0.Aesop.addRappUnsafe]

opaque Aesop.addRapp : Aesop.AddRapp → Aesop.TreeM Aesop.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.