structure Aesop.ExtResult : Type

• depth : Nat
• commonFVarIds : Array Lean.FVarId
• goals : Array (Lean.MVarId × Array Lean.FVarId)

def Aesop.straightLineExt (goal : Lean.MVarId) : Lean.MetaM ExtResult

Equations

• Aesop.straightLineExt goal = Aesop.straightLineExt.go✝ goal 0 #[]

def Aesop.straightLineExtProgress (goal : Lean.MVarId) : Lean.MetaM ExtResult

Equations

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