Documentation

Aesop.Search.Expansion

source
inductive Aesop.RuleResult :
Type
Instances For
    source
    def Aesop.RuleResult.toEmoji :
    RuleResult → String
    Instances For
      source
      def Aesop.RuleResult.isSuccessful :
      RuleResult → Bool
      Instances For
        source
        inductive Aesop.SafeRuleResult :
        Type
        Instances For
          source
          def Aesop.SafeRuleResult.toEmoji :
          SafeRuleResult → String
          Instances For
            source
            def Aesop.SafeRuleResult.isSuccessfulOrPostponed :
            SafeRuleResult → Bool
            Instances For
              source
              def Aesop.runRegularRuleTac (goal : Goal) (tac : RuleTac) (ruleName : RuleName) (indexMatchLocations : Array IndexMatchLocation) (patternSubsts? : Option (Array Substitution)) (options : Options') :
              BaseM (Except Lean.Exception RuleTacOutput)
              Instances For
                source
                def Aesop.addRapps {Q : Type} [Queue Q] (parentRef : GoalRef) (rule : RegularRule) (rapps : Array RuleApplication) :
                SearchM Q RuleResult
                Instances For
                  source
                  @[always_inline]
                  def Aesop.withRuleTraceNode {Q : Type} [Queue Q] {α : Type} (ruleName : RuleName) (toEmoji : α → String) (suffix : String) (k : SearchM Q α) :
                  SearchM Q α
                  Instances For
                    source
                    def Aesop.runRegularRuleCore {Q : Type} [Queue Q] (parentRef : GoalRef) (rule : RegularRule) (indexMatchLocations : Array IndexMatchLocation) (patternSubsts? : Option (Array Substitution)) :
                    SearchM Q (Option RuleTacOutput)
                    Instances For
                      source
                      def Aesop.runSafeRule {Q : Type} [Queue Q] (parentRef : GoalRef) (matchResult : IndexMatchResult SafeRule) :
                      SearchM Q SafeRuleResult
                      Instances For
                        source
                        def Aesop.runUnsafeRule {Q : Type} [Queue Q] (parentRef : GoalRef) (matchResult : IndexMatchResult UnsafeRule) :
                        SearchM Q RuleResult
                        Instances For
                          source
                          inductive Aesop.SafeRulesResult :
                          Type
                          Instances For
                            source
                            def Aesop.SafeRulesResult.toEmoji :
                            SafeRulesResult → String
                            Instances For
                              source
                              def Aesop.runFirstSafeRule {Q : Type} [Queue Q] (gref : GoalRef) :
                              SearchM Q SafeRulesResult
                              Instances For
                                source
                                def Aesop.applyPostponedSafeRule {Q : Type} [Queue Q] (r : PostponedSafeRule) (parentRef : GoalRef) :
                                SearchM Q RuleResult
                                Instances For
                                  source
                                  def Aesop.runFirstUnsafeRule {Q : Type} [Queue Q] (postponedSafeRules : Array PostponedSafeRule) (parentRef : GoalRef) :
                                  SearchM Q RuleResult
                                  Instances For
                                    source
                                    def Aesop.expandGoal {Q : Type} [Queue Q] (gref : GoalRef) :
                                    SearchM Q RuleResult
                                    Instances For