Documentation

Aesop.Search.RuleSelection

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