source
@[specialize #[]]
def Aesop.Script.findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β) (stepOrder : β → Nat) :
Option (Nat × α × β)
Equations

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

Instances For

source
def Aesop.Script.matchGoals (postState₁ postState₂ : Lean.Meta.SavedState) (goals₁ goals₂ : Array Lean.MVarId) :
Lean.MetaM (Option (Std.HashMap Lean.MVarId Lean.MVarId))
Equations

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

Instances For