Documentation

Aesop.Search.RuleSelection

source
def Aesop.selectNormRules (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) :
Aesop.ProfileT Lean.MetaM (Array (Aesop.IndexMatchResult Aesop.NormRule))
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Aesop.preprocessRule :
    Aesop.SafeRule
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Aesop.selectSafeRulesCore {Q : Type} [Aesop.Queue Q] (g : Aesop.Goal) :
      Aesop.SearchM Q (Array (Aesop.IndexMatchResult Aesop.SafeRule))
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.selectSafeRules {Q : Type} [Aesop.Queue Q] (g : Aesop.Goal) :
        Aesop.SearchM Q (Array (Aesop.IndexMatchResult Aesop.SafeRule))
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.selectUnsafeRulesCore {Q : Type} [Aesop.Queue Q] (postponedSafeRules : Array Aesop.PostponedSafeRule) (gref : Aesop.GoalRef) :
          Aesop.SearchM Q Aesop.UnsafeQueue
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Aesop.selectUnsafeRules {Q : Type} [Aesop.Queue Q] (postponedSafeRules : Array Aesop.PostponedSafeRule) (gref : Aesop.GoalRef) :
            Aesop.SearchM Q Aesop.UnsafeQueue
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For