Documentation

Aesop.Util.Basic

theorem Aesop.Array.size_modify {α : Type u_1} (a : Array α) (i : Nat) (f : αα) :
(a.modify i f).size = a.size
@[inline]
def Aesop.time {m : TypeType u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] (x : m α) :
Equations
Instances For
    @[inline]
    def Aesop.time' {m : TypeType u_1} [Monad m] [MonadLiftT BaseIO m] (x : m Unit) :
    Equations
    Instances For
      def Aesop.HashSet.filter {α : Type u_1} [BEq α] [Hashable α] (hs : Lean.HashSet α) (p : αBool) :
      Equations
      Instances For
        @[inline]
        Equations
        Instances For
          @[inline]
          Equations
          Instances For
            def Aesop.instForMHashMapProd_aesop {α : Type u_1} {β : Type u_2} {m : Type u → Type u} [BEq α] [Hashable α] :
            ForM m (Lean.HashMap α β) (α × β)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Aesop.instForInHashMapProd_aesop {α : Type u_1} {β : Type u_2} {m : Type u → Type u} [BEq α] [Hashable α] :
              ForIn m (Lean.HashMap α β) (α × β)
              Equations
              • Aesop.instForInHashMapProd_aesop = { forIn := fun {β_1 : Type u} [Monad m] => ForM.forIn }
              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
                    Equations
                    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
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Aesop.SimpTheorems.foldSimpEntriesM {m : Type u_1 → Type u_1} {σ : 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
                              @[inline]
                              def Aesop.SimpTheorems.foldSimpEntriesM.processTheorem {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (f : σLean.Meta.SimpEntrym σ) (thms : Lean.Meta.SimpTheorems) (s : σ) (thm : Lean.Meta.SimpTheorem) :
                              m σ
                              Equations
                              Instances For
                                def Aesop.SimpTheorems.foldSimpEntries {σ : Type u_1} (f : σLean.Meta.SimpEntryσ) (init : σ) (thms : Lean.Meta.SimpTheorems) :
                                σ
                                Equations
                                Instances For
                                  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
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            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 MVarIds into 'goals' and 'proper mvars'. An MVarId from the input array ms is classified as a proper mvar if any of the ms 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
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Aesop.withAllTransparencySeqSyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) :
                                                              Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
                                                              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.addTryThisTacticSeqSuggestion (ref : Lean.Syntax) (suggestion : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (origSpan? : optParam (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
                                                                        def Aesop.withMaxHeartbeats {m : TypeType u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [MonadWithReaderOf Lean.Core.Context m] (n : Nat) (x : m α) :
                                                                        m α

                                                                        Runs a computation for at most the given number of heartbeats times 1000, ignoring the global heartbeat limit. Note that heartbeats spent on the computation still count towards the global heartbeat count.

                                                                        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