source
structure Aesop.ExtResult :
Type

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

Instances For

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

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

Instances For

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

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

Instances For