structure 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)

def Aesop.RuleApplicationWithMVarInfo.check (preState : Lean.Meta.SavedState) (parentGoal : Lean.MVarId) (r : Aesop.RuleApplicationWithMVarInfo) : Lean.MetaM (Option Lean.MessageData)

Equations

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

def Aesop.RuleApplication.toRuleApplicationWithMVarInfo (parentMVars : Aesop.UnorderedArraySet Lean.MVarId) (r : Aesop.RuleApplication) : Lean.MetaM Aesop.RuleApplicationWithMVarInfo

Equations

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