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 Aesop.ExtResult

Equations

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

partial def Aesop.straightLineExt.go (goal : Lean.MVarId) (depth : Nat) (commonFVarIds : Array Lean.FVarId) : Lean.MetaM Aesop.ExtResult

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

Equations

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