Documentation

Aesop.Search.RuleSelection

source
def Aesop.selectNormRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) :
BaseM (Array (IndexMatchResult NormRule))
Equations
    Instances For
      source
      def Aesop.preprocessRule :
      SafeRule
      Equations
        Instances For
          source
          def Aesop.selectSafeRules {Q : Type} [Queue Q] (g : Goal) :
          SearchM Q (Array (IndexMatchResult SafeRule))
          Equations
            Instances For
              source
              def Aesop.selectUnsafeRules {Q : Type} [Queue Q] (postponedSafeRules : Array PostponedSafeRule) (gref : GoalRef) :
              SearchM Q UnsafeQueue
              Equations
                Instances For