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

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.

def Aesop.Script.matchGoals.getProperGoals (state : Lean.Meta.SavedState) (goals : Array Lean.MVarId) : Lean.MetaM (Array Lean.MVarId)

Equations

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