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 : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] (x : m α) : m (α × Nanos)

Equations

• Aesop.time x = do let start ← liftM IO.monoNanosNow let a ← x let stop ← liftM IO.monoNanosNow pure (a, { nanos := stop - start })

@[inline]

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

Equations

• Aesop.time' x = do let start ← liftM IO.monoNanosNow x let stop ← liftM IO.monoNanosNow pure { nanos := stop - start }

@[inline]

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

Equations

• Aesop.PersistentHashSet.toList s = Lean.PersistentHashSet.fold (fun (as : List α) (a : α) => a :: as) [] s

@[inline]

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

Equations

• Aesop.PersistentHashSet.toArray s = Lean.PersistentHashSet.fold (fun (as : Array α) (a : α) => as.push a) #[] s

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

Equations

• Aesop.PersistentHashSet.toHashSet s = Lean.PersistentHashSet.fold (fun (result : Std.HashSet α) (a : α) => result.insert a) ∅ s

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

Equations

• Aesop.PersistentHashSet.filter p s = Lean.PersistentHashSet.fold (fun (s : Lean.PHashSet α) (a : α) => if p a = true then s else Lean.PersistentHashSet.erase s a) s s

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

Equations

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

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

Equations

• Aesop.instForInHashMapProd_aesop = { forIn := fun {β_1 : Type ?u.44} [Monad m] => ForM.forIn }

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

Equations

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

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

Equations

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

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

Equations

• Aesop.isEmptyTrie (Lean.Meta.DiscrTree.Trie.node vs children) = (vs.isEmpty && children.isEmpty)

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

Equations

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

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.

Equations

• Aesop.filterDiscrTree p f init t = (Aesop.filterDiscrTreeM (fun (a : α) => pure { down := p a }) (fun (s : σ) (a : α) => pure (f s a)) init t).run

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.SimpTheorems.addSimpEntry s (Lean.Meta.SimpEntry.toUnfoldThms n thms) = s.registerDeclToUnfoldThms n thms

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 σ

Equations

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

@[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 σ

Equations

• Aesop.SimpTheorems.foldSimpEntriesM.processTheorem f thms s thm = if Lean.PersistentHashSet.contains thms.erased thm.origin = true then pure s else f s (Lean.Meta.SimpEntry.thm thm)

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

Equations

• Aesop.SimpTheorems.foldSimpEntries f init thms = (Aesop.SimpTheorems.foldSimpEntriesM f init thms).run

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

Equations

• Aesop.SimpTheorems.simpEntries thms = Aesop.SimpTheorems.foldSimpEntries (fun (s : Array Lean.Meta.SimpEntry) (thm : Lean.Meta.SimpEntry) => s.push thm) #[] thms

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

Equations

• Aesop.SimpTheorems.containsDecl thms decl = (thms.isLemma (Lean.Meta.Origin.decl decl) || thms.isDeclToUnfold decl || Lean.PersistentHashMap.contains thms.toUnfoldThms decl)

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

Equations

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

@[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

Equations

• Aesop.forEachExprInLDecl' ldecl g = (Aesop.forEachExprInLDeclCore ldecl g).run

@[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

Equations

• Aesop.forEachExprInLDecl ldecl g = (Aesop.forEachExprInLDeclCore ldecl fun (e : Lean.Expr) => do g e pure true).run

@[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

Equations

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

@[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

Equations

• Aesop.forEachExprInLCtx' mvarId g = mvarId.withContext do let __do_lift ← liftM mvarId.getDecl (Aesop.forEachExprInLCtxCore __do_lift.lctx g).run

@[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

Equations

• Aesop.forEachExprInLCtx mvarId g = Aesop.forEachExprInLCtx' mvarId fun (e : Lean.Expr) => do g e pure true

@[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

Equations

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

@[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

Equations

• Aesop.forEachExprInGoal' mvarId g = (Aesop.forEachExprInGoalCore mvarId g).run

@[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

Equations

• Aesop.forEachExprInGoal mvarId g = Aesop.forEachExprInGoal' mvarId fun (e : Lean.Expr) => do g e pure true

@[inline]

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

Equations

• Aesop.setThe σ s = set s

@[inline]

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

Equations

• Aesop.runMetaMAsCoreM x = Prod.fst <$> x.run

@[inline]

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

Equations

• Aesop.runTermElabMAsCoreM x = Aesop.runMetaMAsCoreM x.run'

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

Equations

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

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

Equations

• Aesop.runTacticSyntaxAsMetaM stx goals = do let __do_lift ← Aesop.runTacticMAsMetaM (Lean.Elab.Tactic.evalTactic stx) goals pure __do_lift.snd

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.updateSimpEntryPriority priority (Lean.Meta.SimpEntry.toUnfoldThms a a_1) = Lean.Meta.SimpEntry.toUnfoldThms a a_1
• Aesop.updateSimpEntryPriority priority (Lean.Meta.SimpEntry.toUnfold a) = Lean.Meta.SimpEntry.toUnfold a

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

Equations

• Aesop.getMVarDependencies e = do let __discr ← (Lean.MVarId.getMVarDependencies.addMVars true e).run ∅ match __discr with | (fst, deps) => pure deps

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

Equations

• Aesop.hasSorry e = do let __do_lift ← Lean.getMCtx pure (Aesop.hasSorry.go __do_lift e)

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

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

Equations

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

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

Equations

• Aesop.getAppUpToDefeq e = Aesop.getAppUpToDefeq.go #[] e

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.

Equations

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

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)

Equations

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

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

Equations

• Aesop.runTacticCapturingPostState t preState preGoals = Aesop.runTacticMCapturingPostState (Lean.Elab.Tactic.evalTactic t.raw) preState preGoals

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)

Equations

• Aesop.runTacticSeqCapturingPostState t preState preGoals = Aesop.runTacticMCapturingPostState (Lean.Elab.Tactic.evalTactic t.raw) preState preGoals

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

Equations

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

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.
• Aesop.withTransparencySeqSyntax Lean.Meta.TransparencyMode.default k = (pure k).run

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.
• Aesop.withAllTransparencySeqSyntax md k = k

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.withTransparencySyntax Lean.Meta.TransparencyMode.default k = (pure k).run

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.withAllTransparencySyntax md k = k

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.

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

• Aesop.elabPattern stx = Lean.withRef stx (withReader Aesop.elabPattern.adjustCtx (Lean.Elab.Term.withSynthesize (Lean.Elab.Term.elabTerm stx none)))

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

Equations

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

opaque Aesop.aesop.smallErrorMessages : Lean.Option Bool

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

Equations

• Aesop.tacticsToMessageData ts = Lean.MessageData.joinSep (Array.map Lean.toMessageData ts).toList ((Lean.MessageData.ofFormat ∘ Std.format) "\n")

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

Note: the returned local context contains invalid LocalDecls.

Equations

• Aesop.getUnusedNames lctx suggestions = Aesop.getUnusedNames.go suggestions 0 (Array.mkEmpty suggestions.size) lctx

@[irreducible]

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

Equations

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

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

Equations

• Aesop.getUnusedNames.dummyLDecl name = Lean.LocalDecl.cdecl 0 { name := `_ } name (Lean.Expr.sort Lean.levelZero) Lean.BinderInfo.default Lean.LocalDeclKind.default

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

Equations

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

@[macro_inline]

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

Equations

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

@[macro_inline]

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

Equations

• Aesop.withExceptionPrefix pre = Aesop.withExceptionTransform fun (msg : Lean.MessageData) => pre ++ msg

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

Equations

• Aesop.withPPAnalyze x = Lean.withOptions (fun (x : Lean.Options) => (Lean.KVMap.setBool x `pp.analyze true).setBool `pp.proofs true) x

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

Equations

• Aesop.instMonadCacheStateRefT'_aesop = { findCached? := fun (a : α) => liftM (Lean.MonadCache.findCached? a), cache := fun (a : α) (b : β) => liftM (Lean.MonadCache.cache a b) }

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

Equations

• Aesop.runInMetaState s x = do let initialState ← let_fun this := Lean.saveState; liftM this tryFinally (do liftM s.restore x) (liftM initialState.restore)

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

Equations

• Aesop.lBoolOr Lean.LBool.true x✝ = Lean.LBool.true
• Aesop.lBoolOr Lean.LBool.false x✝ = x✝
• Aesop.lBoolOr Lean.LBool.undef Lean.LBool.true = Lean.LBool.true
• Aesop.lBoolOr Lean.LBool.undef x✝ = Lean.LBool.undef

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

Equations

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

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

Equations

• Aesop.compareArraySizeThenLex cmp xs ys = (compare xs.size ys.size).then (Aesop.compareArrayLex cmp xs ys)