source
@[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 })

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

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

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

source
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.

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[inline]
def Aesop.runMetaMAsCoreM {α : Type} (x : Lean.MetaM α) :
Lean.CoreM α
Equations

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

Instances For

source
@[inline]
def Aesop.runTermElabMAsCoreM {α : Type} (x : Lean.Elab.TermElabM α) :
Lean.CoreM α
Equations

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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

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

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

Instances For

source
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

Instances For

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

Partition an array of structures containing `MVarId`s into 'goals' and 'proper mvars'. An `MVarId` from the input array `goals` is classified as a proper mvar if any of the `MVarId`s 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

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
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)))

Instances For

source
opaque Aesop.aesop.smallErrorMessages :
Lean.Option Bool
source
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")

Instances For

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

Note: the returned local context contains invalid `LocalDecl`s.

Equations

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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) }

Instances For

source
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)

Instances For

source
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

Instances For

source
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.

Instances For

source
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)

Instances For