@[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.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.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_2} {σ : 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_2} {σ : 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

• Aesop.runTacticMAsMetaM x goals = do let __discr ← ((ReaderT.run x { elaborator := Lean.Name.anonymous }).run { goals := goals }).run' match __discr with | (a, s) => pure (a, s.goals)

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.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.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 ← have 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)