Documentation

Aesop.Search.SearchM

source
structure Aesop.NormSimpContext :
Type
Instances For
    source
    def Aesop.instInhabitedNormSimpContext.default :
    NormSimpContext
    Instances For
      source
      @[implicit_reducible]
      instance Aesop.instInhabitedNormSimpContext :
      Inhabited NormSimpContext
      source
      structure Aesop.SearchM.Context :
      Type
      Instances For
        source
        instance Aesop.SearchM.instNonemptyContext :
        Nonempty Context
        source
        structure Aesop.SearchM.State (Q : Type) [Queue Q] :
        Type
        • iteration : Iteration
        • queue : Q
        • maxRuleApplicationDepthReached : Bool
        Instances For
          source
          @[implicit_reducible]
          instance Aesop.SearchM.instInhabitedState {a✝ : Type} [Inhabited a✝] {a✝¹ : Queue a✝} :
          Inhabited (State a✝)
          source
          def Aesop.SearchM.instInhabitedState.default {a✝ : Type} [Inhabited a✝] {a✝¹ : Queue a✝} :
          State a✝
          Instances For
            source
            @[reducible, inline]
            abbrev Aesop.SearchM (Q : Type) [Queue Q] (α : Type) :
            Type
            Instances For
              source
              @[implicit_reducible]
              instance Aesop.SearchM.instMonad {Q : Type} [Queue Q] :
              Monad (SearchM Q)
              source
              @[implicit_reducible]
              instance Aesop.SearchM.instMonadRef {Q : Type} [Queue Q] :
              Lean.MonadRef (SearchM Q)
              source
              @[implicit_reducible]
              instance Aesop.SearchM.instInhabited {Q : Type} [Queue Q] {α : Type} :
              Inhabited (SearchM Q α)
              source
              @[implicit_reducible]
              instance Aesop.SearchM.instMonadStateState {Q : Type} [Queue Q] :
              MonadState (State Q) (SearchM Q)
              source
              @[implicit_reducible]
              instance Aesop.SearchM.instMonadReaderContext {Q : Type} [Queue Q] :
              MonadReader Context (SearchM Q)
              source
              @[implicit_reducible]
              instance Aesop.SearchM.instMonadLiftTreeM {Q : Type} [Queue Q] :
              MonadLift TreeM (SearchM Q)
              source
              def Aesop.SearchM.run' {Q : Type} [Queue Q] {α : Type} (ctx : Context) (σ : State Q) (tree : Tree) (x : SearchM Q α) :
              BaseM (α × State Q × Tree)
              Instances For
                source
                def Aesop.SearchM.run {Q : Type} [Queue Q] {α : Type} (ruleSet : LocalRuleSet) (options : Options') (simpConfig : Lean.Meta.Simp.Config) (simpConfigStx? : Option Lean.Term) (goal : Lean.MVarId) (x : SearchM Q α) :
                BaseM (α × State Q × Tree)
                Instances For
                  source
                  def Aesop.getTree {Q : Type} [Queue Q] :
                  SearchM Q Tree
                  Instances For
                    source
                    def Aesop.setTree {Q : Type} [Queue Q] :
                    Tree → SearchM Q Unit
                    Instances For
                      source
                      def Aesop.modifyTree {Q : Type} [Queue Q] :
                      (Tree → Tree) → SearchM Q Unit
                      Instances For
                        source
                        def Aesop.getIteration {Q : Type} [Queue Q] :
                        SearchM Q Iteration
                        Instances For
                          source
                          def Aesop.incrementIteration {Q : Type} [Queue Q] :
                          SearchM Q Unit
                          Instances For
                            source
                            def Aesop.popGoal? {Q : Type} [Queue Q] :
                            SearchM Q (Option GoalRef)
                            Instances For
                              source
                              def Aesop.enqueueGoals {Q : Type} [Queue Q] (gs : Array GoalRef) :
                              SearchM Q Unit
                              Instances For
                                source
                                def Aesop.setMaxRuleApplicationDepthReached {Q : Type} [Queue Q] :
                                SearchM Q Unit
                                Instances For
                                  source
                                  def Aesop.wasMaxRuleApplicationDepthReached {Q : Type} [Queue Q] :
                                  SearchM Q Bool
                                  Instances For