Documentation

Aesop.ElabM

source
structure Aesop.ElabM.Context :
Type
Instances For
    source
    def Aesop.ElabM.Context.forAdditionalRules (goal : Lean.MVarId) :
    Context
    Instances For
      source
      def Aesop.ElabM.Context.forAdditionalGlobalRules :
      Lean.MetaM Context
      Instances For
        source
        def Aesop.ElabM.Context.forErasing (goal : Lean.MVarId) :
        Context
        Instances For
          source
          def Aesop.ElabM.Context.forGlobalErasing :
          Lean.MetaM Context
          Instances For
            source
            @[reducible, inline]
            abbrev Aesop.ElabM (α : Type) :
            Type
            Instances For
              source
              @[implicit_reducible]
              instance Aesop.instMonadElabM :
              Monad ElabM
              source
              def Aesop.ElabM.run {α : Type} (ctx : Context) (x : ElabM α) :
              Lean.Elab.TermElabM α
              Instances For
                source
                def Aesop.shouldParsePriorities :
                ElabM Bool
                Instances For
                  source
                  def Aesop.getGoal :
                  ElabM Lean.MVarId
                  Instances For