HepLean Documentation

Aesop.Script.Util

source
@[specialize #[]]
def Aesop.Script.findFirstStep? {α : Type} {β : 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₁ : Lean.Meta.SavedState) (postState₂ : Lean.Meta.SavedState) (goals₁ : Array Lean.MVarId) (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
      source
      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.
      Instances For