@[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
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.