def Aesop.Subarray.popFront? {α : Type u_1} (as : Subarray α) : Option (α × Subarray α)

Equations

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

@[inline]

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

Equations

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

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

Equations

• Aesop.HashSet.filter hs p = Lean.HashSet.fold (fun hs a => if p a = true then Lean.HashSet.insert hs a else hs) ∅ hs

@[inline]

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

Equations

• Aesop.PersistentHashSet.toList s = Lean.PersistentHashSet.fold (fun as 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 a => Array.push as a) (Array.mkEmpty (Lean.PersistentHashSet.size s)) s

def Aesop.getConclusionDiscrTreeKeys {s : Bool} (type : Lean.Expr) : Lean.MetaM (Array (Lean.Meta.DiscrTree.Key s))

Equations

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

def Aesop.getConstDiscrTreeKeys {s : Bool} (decl : Lean.Name) : Lean.MetaM (Array (Lean.Meta.DiscrTree.Key s))

Equations

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

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

Equations

• Aesop.isEmptyTrie x = match x with | Lean.Meta.DiscrTree.Trie.node vs children => Array.isEmpty vs && Array.isEmpty children

@[specialize #[]]

def Aesop.filterDiscrTreeM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} {s : Bool} [Monad m] [Inhabited σ] (p : α → m (ULift Bool)) (f : σ → α → m σ) (init : σ) (t : Lean.Meta.DiscrTree α s) : m (Lean.Meta.DiscrTree α s × σ)

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

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 = Id.run (Aesop.filterDiscrTreeM (fun a => pure { down := p a }) (fun s a => pure (f s a)) init t)

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.

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

Equations

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

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 = Id.run (Aesop.SimpTheorems.foldSimpEntriesM f init thms)

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

Equations

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

def Aesop.SimpTheorems.merge (s : Lean.Meta.SimpTheorems) (t : Lean.Meta.SimpTheorems) : Lean.Meta.SimpTheorems

Equations

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

def Aesop.SimpTheorems.merge.mkErased (s : Lean.Meta.SimpTheorems) (t : Lean.Meta.SimpTheorems) (init : Lean.PHashSet Lean.Meta.Origin) : Lean.PHashSet Lean.Meta.Origin

Equations

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

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

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

@[inline]

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

Equations

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

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.

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

Equations

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

def Aesop.partitionGoalsAndMVars (goals : Array Lean.MVarId) : Lean.MetaM (Array (Lean.MVarId × Aesop.UnorderedArraySet Lean.MVarId) × Aesop.UnorderedArraySet Lean.MVarId)

Partition an array of MVarIds into 'goals' and 'proper mvars'. An MVarId from the input array ms is classified as a proper mvar if any of the ms 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.withTransparencySeqSyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) : m (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def Aesop.withAllTransparencySeqSyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) : m (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def Aesop.withTransparencySyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `tactic) : m (Lean.TSyntax `tactic)

Equations

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

def Aesop.withAllTransparencySyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (md : Lean.Meta.TransparencyMode) (k : Lean.TSyntax `tactic) : m (Lean.TSyntax `tactic)

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)