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
            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
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[inline]
                                    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
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          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