structure Aesop.AddRappextends Aesop.RuleApplicationWithMVarInfo : Type

• postState : Lean.Meta.SavedState
• originalSubgoals : Array Lean.MVarId
• goals : Array (Lean.MVarId × Aesop.UnorderedArraySet Lean.MVarId)
• mvars : Aesop.UnorderedArraySet Lean.MVarId
• introducedMVars : Aesop.UnorderedArraySet Lean.MVarId
• assignedMVars : Aesop.UnorderedArraySet Lean.MVarId
• scriptBuilder? : Option (Aesop.ScriptBuilder Lean.MetaM)
• 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