Documentation

Aesop.Util.Basic

@[inline]
def Aesop.time {m : TypeType u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] (x : m α) :
m (α × Nanos)
Equations
Instances For
    @[inline]
    def Aesop.time' {m : TypeType u_1} [Monad m] [MonadLiftT BaseIO m] (x : m Unit) :
    Equations
    Instances For
      @[inline]
      Equations
      Instances For
        @[inline]
        Equations
        Instances For
          Equations
          Instances For
            def Aesop.PersistentHashSet.filter {α : Type u_1} [BEq α] [Hashable α] (p : αBool) (s : Lean.PHashSet α) :
            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[specialize #[]]
                def Aesop.filterDiscrTreeM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] [Inhabited σ] (p : αm (ULift Bool)) (f : σαm σ) (init : σ) (t : Lean.Meta.DiscrTree α) :

                Remove elements for which p returns false from the given DiscrTree. The removed elements are monadically folded over using f and init, so f is called once for each removed element and the final state of type σ is returned.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Aesop.filterDiscrTree {σ : Type u_1} {α : Type} [Inhabited σ] (p : αBool) (f : σασ) (init : σ) (t : Lean.Meta.DiscrTree α) :

                  Remove elements for which p returns false from the given DiscrTree. The removed elements are folded over using f and init, so f is called once for each removed element and the final state of type σ is returned.

                  Equations
                  Instances For
                    def Aesop.SimpTheorems.foldSimpEntriesM {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (f : σLean.Meta.SimpEntrym σ) (init : σ) (thms : Lean.Meta.SimpTheorems) :
                    m σ
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Aesop.SimpTheorems.foldSimpEntries {σ : Type u_1} (f : σLean.Meta.SimpEntryσ) (init : σ) (thms : Lean.Meta.SimpTheorems) :
                      σ
                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[always_inline]
                          def Aesop.forEachExprInLDecl' {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (ldecl : Lean.LocalDecl) (g : Lean.Exprm Bool) :
                          Equations
                          Instances For
                            @[always_inline]
                            def Aesop.forEachExprInLDecl {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (ldecl : Lean.LocalDecl) (g : Lean.Exprm Unit) :
                            Equations
                            Instances For
                              @[always_inline]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[always_inline]
                                def Aesop.forEachExprInLCtx' {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Exprm Bool) :
                                Equations
                                Instances For
                                  @[always_inline]
                                  def Aesop.forEachExprInLCtx {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Exprm Unit) :
                                  Equations
                                  Instances For
                                    @[always_inline]
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[always_inline]
                                      def Aesop.forEachExprInGoal' {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Exprm Bool) :
                                      Equations
                                      Instances For
                                        @[always_inline]
                                        def Aesop.forEachExprInGoal {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Exprm Unit) :
                                        Equations
                                        Instances For
                                          @[inline]
                                          def Aesop.setThe (σ : Type u_1) {m : Type u_1 → Type u_2} [MonadStateOf σ m] (s : σ) :
                                          Equations
                                          Instances For
                                            @[inline]
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For
                                                def Aesop.hasSorry {m : TypeType} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) :
                                                Equations
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    If the input expression e reduces to f x₁ ... xₙ via repeated whnf, this function returns f and [x₁, ⋯, xₙ]. Otherwise it returns e (unchanged, not in WHNF!) and [].

                                                    Equations
                                                    Instances For

                                                      Partition an array of structures containing MVarIds into 'goals' and 'proper mvars'. An MVarId from the input array goals is classified as a proper mvar if any of the MVarIds depend on it, and as a goal otherwise. Additionally, for each goal, we report the set of mvars that the goal depends on.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def Aesop.withTransparencySeqSyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) :
                                                            Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
                                                            Equations
                                                            Instances For
                                                              def Aesop.withAllTransparencySeqSyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) :
                                                              Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
                                                              Equations
                                                              Instances For
                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  Instances For
                                                                    def Aesop.addTryThisTacticSeqSuggestion (ref : Lean.Syntax) (suggestion : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (origSpan? : Option Lean.Syntax := none) :

                                                                    Register a "Try this" suggestion for a tactic sequence.

                                                                    It works when the tactic to replace appears on its own line:

                                                                    by
                                                                      aesop?
                                                                    

                                                                    It doesn't work (i.e., the suggestion will appear but in the wrong place) when the tactic to replace is preceded by other text on the same line:

                                                                    have x := by aesop?
                                                                    

                                                                    The Try this: suggestion in the infoview is not correctly formatted, but there's nothing we can do about this at the moment.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          Note: the returned local context contains invalid LocalDecls.

                                                                          Equations
                                                                          Instances For
                                                                            @[irreducible]
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[macro_inline]
                                                                                def Aesop.withExceptionTransform {m : TypeType} {α : Type} [Monad m] [Lean.MonadError m] (f : Lean.MessageDataLean.MessageData) (x : m α) :
                                                                                m α
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[macro_inline]
                                                                                  def Aesop.withExceptionPrefix {m : TypeType} {α : Type} [Monad m] [Lean.MonadError m] (pre : Lean.MessageData) :
                                                                                  m αm α
                                                                                  Equations
                                                                                  Instances For
                                                                                    def Aesop.withPPAnalyze {m : TypeType} {α : Type} [Monad m] [Lean.MonadWithOptions m] (x : m α) :
                                                                                    m α
                                                                                    Equations
                                                                                    Instances For
                                                                                      def Aesop.instMonadCacheStateRefT'_aesop {α β : Type} {m : TypeType} {ω σ : Type} [Lean.MonadCache α β m] :
                                                                                      Lean.MonadCache α β (StateRefT' ω σ m)
                                                                                      Equations
                                                                                      Instances For
                                                                                        def Aesop.runInMetaState {m : TypeType u_1} {α : Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] (s : Lean.Meta.SavedState) (x : m α) :
                                                                                        m α

                                                                                        A generalized variant of Meta.SavedState.runMetaM

                                                                                        Equations
                                                                                        Instances For
                                                                                          def Aesop.compareArrayLex {α : Type u_1} (cmp : ααOrdering) (xs ys : Array α) :
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            def Aesop.compareArraySizeThenLex {α : Type u_1} (cmp : ααOrdering) (xs ys : Array α) :
                                                                                            Equations
                                                                                            Instances For