@[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.getConclusionDiscrTreeKeys (type : Lean.Expr) : 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_2} {σ : Type u_1} [Monad m] (f : σ → Lean.Meta.SimpEntry → m σ) (init : σ) (thms : Lean.Meta.SimpTheorems) : 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.hasSorry {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) : m 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 [].

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.withAllTransparencySeqSyntax (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq

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.elabPattern (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

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.

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

def Aesop.instMonadParentDeclReaderT_aesop {m : Type → Type} {ρ : Type} [Lean.Elab.MonadParentDecl m] : Lean.Elab.MonadParentDecl (ReaderT ρ m)

def Aesop.instMonadParentDeclStateRefT'_aesop {m : Type → Type} {ω σ : Type} [Lean.Elab.MonadParentDecl m] : Lean.Elab.MonadParentDecl (StateRefT' ω σ m)

def Aesop.isDefEqReducibleRigid (s t : Lean.Expr) : Lean.MetaM Bool

def Aesop.isHypRedundantReducibleRigid (type : Lean.Expr) : Lean.MetaM Bool