@[inline]

def Aesop.time {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] (x : m α) : m (α × Nanos)

@[inline]

def Aesop.time' {m : Type → Type u_1} [Monad m] [MonadLiftT BaseIO m] (x : m Unit) : m Nanos

@[inline]

def Aesop.PersistentHashSet.toList {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PersistentHashSet α) : List α

@[inline]

def Aesop.PersistentHashSet.toArray {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PersistentHashSet α) : Array α

def Aesop.PersistentHashSet.toHashSet {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PHashSet α) : Std.HashSet α

def Aesop.PersistentHashSet.filter {α : Type u_1} [BEq α] [Hashable α] (p : α → Bool) (s : Lean.PHashSet α) : Lean.PHashSet α

def Aesop.instForMHashMapProd_aesop {α : Type u_1} {β : Type u_2} {m : Type u → Type u} [BEq α] [Hashable α] : ForM m (Std.HashMap α β) (α × β)

def Aesop.instForInHashMapProd_aesop {α : Type u_1} {β : Type u_2} {m : Type u → Type u} [BEq α] [Hashable α] : ForIn m (Std.HashMap α β) (α × β)

def Aesop.getConclusionDiscrTreeKeys (type : Lean.Expr) : Lean.MetaM (Array Lean.Meta.DiscrTree.Key)

def Aesop.getConstDiscrTreeKeys (decl : Lean.Name) : Lean.MetaM (Array Lean.Meta.DiscrTree.Key)

def Aesop.isEmptyTrie {α : Type} : Lean.Meta.DiscrTree.Trie α → Bool

@[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 α) : m (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.

def Aesop.filterDiscrTree {σ : Type u_1} {α : Type} [Inhabited σ] (p : α → Bool) (f : σ → α → σ) (init : σ) (t : Lean.Meta.DiscrTree α) : 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.

def Aesop.SimpTheorems.addSimpEntry (s : Lean.Meta.SimpTheorems) : Lean.Meta.SimpEntry → Lean.Meta.SimpTheorems

def Aesop.SimpTheorems.foldSimpEntriesM {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (f : σ → Lean.Meta.SimpEntry → m σ) (init : σ) (thms : Lean.Meta.SimpTheorems) : m σ

@[inline]

def Aesop.SimpTheorems.foldSimpEntriesM.processTheorem {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (f : σ → Lean.Meta.SimpEntry → m σ) (thms : Lean.Meta.SimpTheorems) (s : σ) (thm : Lean.Meta.SimpTheorem) : m σ

def Aesop.SimpTheorems.foldSimpEntries {σ : Type u_1} (f : σ → Lean.Meta.SimpEntry → σ) (init : σ) (thms : Lean.Meta.SimpTheorems) : σ

def Aesop.SimpTheorems.simpEntries (thms : Lean.Meta.SimpTheorems) : Array Lean.Meta.SimpEntry

def Aesop.SimpTheorems.containsDecl (thms : Lean.Meta.SimpTheorems) (decl : Lean.Name) : Bool

def Aesop.forEachExprInLDeclCore {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (ldecl : Lean.LocalDecl) (g : Lean.Expr → m Bool) : Lean.MonadCacheT Lean.Expr Unit m Unit

@[always_inline]

def Aesop.forEachExprInLDecl' {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (ldecl : Lean.LocalDecl) (g : Lean.Expr → m Bool) : m Unit

@[always_inline]

def Aesop.forEachExprInLDecl {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (ldecl : Lean.LocalDecl) (g : Lean.Expr → m Unit) : m Unit

@[always_inline]

def Aesop.forEachExprInLCtxCore {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (lctx : Lean.LocalContext) (g : Lean.Expr → m Bool) : Lean.MonadCacheT Lean.Expr Unit m Unit

@[always_inline]

def Aesop.forEachExprInLCtx' {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Bool) : m Unit

@[always_inline]

def Aesop.forEachExprInLCtx {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Unit) : m Unit

@[always_inline]

def Aesop.forEachExprInGoalCore {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Bool) : Lean.MonadCacheT Lean.Expr Unit m Unit

@[always_inline]

def Aesop.forEachExprInGoal' {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Bool) : m Unit

@[always_inline]

def Aesop.forEachExprInGoal {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] [MonadControlT Lean.MetaM m] [MonadLiftT Lean.MetaM m] (mvarId : Lean.MVarId) (g : Lean.Expr → m Unit) : m Unit

@[inline]

def Aesop.setThe (σ : Type u_1) {m : Type u_1 → Type u_2} [MonadStateOf σ m] (s : σ) : m PUnit

@[inline]

def Aesop.runMetaMAsCoreM {α : Type} (x : Lean.MetaM α) : Lean.CoreM α

@[inline]

def Aesop.runTermElabMAsCoreM {α : Type} (x : Lean.Elab.TermElabM α) : Lean.CoreM α

def Aesop.runTacticMAsMetaM {α : Type} (x : Lean.Elab.Tactic.TacticM α) (goals : List Lean.MVarId) : Lean.MetaM (α × List Lean.MVarId)

def Aesop.runTacticSyntaxAsMetaM (stx : Lean.Syntax) (goals : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

def Aesop.updateSimpEntryPriority (priority : Nat) (e : Lean.Meta.SimpEntry) : Lean.Meta.SimpEntry

def Aesop.getMVarDependencies (e : Lean.Expr) : Lean.MetaM (Std.HashSet Lean.MVarId)

def Aesop.hasSorry {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) : m Bool

partial def Aesop.hasSorry.go (mctx : Lean.MetavarContext) (e : Lean.Expr) : Bool

def Aesop.isAppOfUpToDefeq (f e : Lean.Expr) : Lean.MetaM Bool

def Aesop.getAppUpToDefeq (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.Expr)

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 [].

partial def Aesop.getAppUpToDefeq.go (args : Array Lean.Expr) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.Expr)

def Aesop.partitionGoalsAndMVars {α : Type} (mvarId : α → Lean.MVarId) (goals : Array α) : Lean.MetaM (Array (α × UnorderedArraySet Lean.MVarId) × UnorderedArraySet Lean.MVarId)

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.

def Aesop.runTacticMCapturingPostState (t : Lean.Elab.Tactic.TacticM Unit) (preState : Lean.Meta.SavedState) (preGoals : List Lean.MVarId) : Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)

def Aesop.runTacticCapturingPostState (t : Lean.Syntax.Tactic) (preState : Lean.Meta.SavedState) (preGoals : List Lean.MVarId) : Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)

def Aesop.runTacticSeqCapturingPostState (t : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (preState : Lean.Meta.SavedState) (preGoals : List Lean.MVarId) : Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)

def Aesop.runTacticsCapturingPostState (ts : Array Lean.Syntax.Tactic) (preState : Lean.Meta.SavedState) (preGoals : List Lean.MVarId) : Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)

def Aesop.withTransparencySeqSyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq

def Aesop.withAllTransparencySeqSyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq

def Aesop.withTransparencySyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `tactic) : Lean.TSyntax `tactic

def Aesop.withAllTransparencySyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `tactic) : Lean.TSyntax `tactic

def Aesop.addTryThisTacticSeqSuggestion (ref : Lean.Syntax) (suggestion : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (origSpan? : Option Lean.Syntax := none) : Lean.MetaM Unit

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.

def Aesop.addTryThisTacticSeqSuggestion.dedent (s : String) : String

def Aesop.withMaxHeartbeats {m : Type → Type 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.

def Aesop.withAtMostMaxHeartbeats {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [MonadLiftT Lean.CoreM m] [MonadWithReaderOf Lean.Core.Context m] (n : Nat) (x : m α) : m α

Runs a computation for at most the given number of heartbeats times 1000 or the global heartbeat limit, whichever is lower. Note that heartbeats spent on the computation still count towards the global heartbeat count. If 0 is given, the global heartbeat limit is used.

def Aesop.elabPattern (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

def Aesop.elabPattern.adjustCtx (old : Lean.Elab.Term.Context) : Lean.Elab.Term.Context

opaque Aesop.aesop.smallErrorMessages : Lean.Option Bool

def Aesop.tacticsToMessageData (ts : Array Lean.Syntax.Tactic) : Lean.MessageData

def Aesop.getUnusedNames (lctx : Lean.LocalContext) (suggestions : Array Lean.Name) : Array Lean.Name × Lean.LocalContext

Note: the returned local context contains invalid LocalDecls.

@[irreducible]

def Aesop.getUnusedNames.go (suggestions : Array Lean.Name) (i : Nat) (acc : Array Lean.Name) (lctx : Lean.LocalContext) : Array Lean.Name × Lean.LocalContext

def Aesop.getUnusedNames.dummyLDecl (name : Lean.Name) : Lean.LocalDecl

def Aesop.Name.ofComponents (cs : List Lean.Name) : Lean.Name

@[macro_inline]

def Aesop.withExceptionTransform {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (f : Lean.MessageData → Lean.MessageData) (x : m α) : m α

@[macro_inline]

def Aesop.withExceptionPrefix {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (pre : Lean.MessageData) : m α → m α

def Aesop.withPPAnalyze {m : Type → Type} {α : Type} [Monad m] [Lean.MonadWithOptions m] (x : m α) : m α

def Aesop.instMonadCacheStateRefT'_aesop {α β : Type} {m : Type → Type} {ω σ : Type} [Lean.MonadCache α β m] : Lean.MonadCache α β (StateRefT' ω σ m)

def Aesop.runInMetaState {m : Type → Type 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

def Aesop.lBoolOr (x y : Lean.LBool) : Lean.LBool

def Aesop.compareArrayLex {α : Type u_1} (cmp : α → α → Ordering) (xs ys : Array α) : Ordering

def Aesop.compareArraySizeThenLex {α : Type u_1} (cmp : α → α → Ordering) (xs ys : Array α) : Ordering