Documentation

Aesop.Search.SearchM

source
structure Aesop.NormSimpContext :
Type
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
        @[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