- depth : Nat
- commonFVarIds : Array Lean.FVarId
- goals : Array (Lean.MVarId × Array Lean.FVarId)
Instances For
partial def
Aesop.straightLineExt.go
(goal : Lean.MVarId)
(depth : Nat)
(commonFVarIds : Array Lean.FVarId)
:
Equations
- One or more equations did not get rendered due to their size.