Loogle!

Result

Found 27 declarations mentioning Std.Queue.

• Std.Queue 📋 Init.Data.Queue
  (α : Type u) : Type u
• Std.Queue.empty 📋 Init.Data.Queue
  {α : Type u} : Std.Queue α
• Std.Queue.instEmptyCollection 📋 Init.Data.Queue
  {α : Type u} : EmptyCollection (Std.Queue α)
• Std.Queue.instInhabited 📋 Init.Data.Queue
  {α : Type u} : Inhabited (Std.Queue α)
• Std.Queue.isEmpty 📋 Init.Data.Queue
  {α : Type u} (q : Std.Queue α) : Bool
• Std.Queue.dList 📋 Init.Data.Queue
  {α : Type u} (self : Std.Queue α) : List α
• Std.Queue.eList 📋 Init.Data.Queue
  {α : Type u} (self : Std.Queue α) : List α
• Std.Queue.toArray 📋 Init.Data.Queue
  {α : Type u} (q : Std.Queue α) : Array α
• Std.Queue.enqueue 📋 Init.Data.Queue
  {α : Type u} (v : α) (q : Std.Queue α) : Std.Queue α
• Std.Queue.enqueueAll 📋 Init.Data.Queue
  {α : Type u} (vs : List α) (q : Std.Queue α) : Std.Queue α
• Std.Queue.mk 📋 Init.Data.Queue
  {α : Type u} (eList dList : List α) : Std.Queue α
• Std.Queue.dequeue? 📋 Init.Data.Queue
  {α : Type u} (q : Std.Queue α) : Option (α × Std.Queue α)
• Std.Queue.filterM 📋 Init.Data.Queue
  {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (q : Std.Queue α) : m (Std.Queue α)
• _private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.values 📋 Std.Sync.Channel
  {α : Type} (self : Std.CloseableChannel.Unbounded.State✝ α) : Std.Queue α
• _private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.consumers 📋 Std.Sync.Channel
  {α : Type} (self : Std.CloseableChannel.Bounded.State✝ α) : Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)
• _private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.producers 📋 Std.Sync.Channel
  {α : Type} (self : Std.CloseableChannel.Bounded.State✝ α) : Std.Queue (IO.Promise Bool)
• _private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.consumers 📋 Std.Sync.Channel
  {α : Type} (self : Std.CloseableChannel.Unbounded.State✝ α) : Std.Queue (Std.CloseableChannel.Consumer✝ α)
• _private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.consumers 📋 Std.Sync.Channel
  {α : Type} (self : Std.CloseableChannel.Zero.State✝ α) : Std.Queue (Std.CloseableChannel.Consumer✝ α)
• _private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.producers 📋 Std.Sync.Channel
  {α : Type} (self : Std.CloseableChannel.Zero.State✝ α) : Std.Queue (α × IO.Promise Bool)
• Std.Notify.State.consumers 📋 Std.Sync.Notify
  (self : Std.Notify.State) : Std.Queue (Std.Notify.Consumer Unit)
• Std.Notify.State.mk 📋 Std.Sync.Notify
  (consumers : Std.Queue (Std.Notify.Consumer Unit)) : Std.Notify.State
• _private.Std.Sync.Broadcast.0.Std.Bounded.State.producers 📋 Std.Sync.Broadcast
  {α : Type} (self : Std.Bounded.State✝ α) : Std.Queue (IO.Promise Bool)
• _private.Std.Sync.Broadcast.0.Std.Bounded.State.waiters 📋 Std.Sync.Broadcast
  {α : Type} (self : Std.Bounded.State✝ α) : Std.Queue (Std.Broadcast.Consumer✝ α)
• Std.CancellationToken.State.consumers 📋 Std.Sync.CancellationToken
  (self : Std.CancellationToken.State) : Std.Queue Std.CancellationToken.Consumer
• Std.CancellationToken.State.mk 📋 Std.Sync.CancellationToken
  (reason : Option Std.CancellationReason) (consumers : Std.Queue Std.CancellationToken.Consumer) : Std.CancellationToken.State
• Lean.Meta.Grind.GoalState.newRawFacts 📋 Lean.Meta.Tactic.Grind.Types
  (self : Lean.Meta.Grind.GoalState) : Std.Queue Lean.Meta.Grind.NewRawFact
• Lean.Meta.Grind.GoalState.mk 📋 Lean.Meta.Tactic.Grind.Types
  (nextDeclIdx : ℕ) (canon : Lean.Meta.Grind.Canon.State) (enodeMap : Lean.Meta.Grind.ENodeMap) (exprs : Lean.PArray Lean.Expr) (parents : Lean.Meta.Grind.ParentMap) (congrTable : Lean.Meta.Grind.CongrTable enodeMap) (appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (indicesFound : Lean.PHashSet Lean.HeadIndex) (newFacts : Array Lean.Meta.Grind.NewFact) (inconsistent : Bool) (nextIdx : ℕ) (newRawFacts : Std.Queue Lean.Meta.Grind.NewRawFact) (facts : Lean.PArray Lean.Expr) (extThms : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem)) (ematch : Lean.Meta.Grind.EMatch.State) (inj : Lean.Meta.Grind.Injective.State) (split : Lean.Meta.Grind.Split.State) (clean : Lean.Meta.Grind.Clean.State) (sstates : Array Lean.Meta.Grind.SolverExtensionState) : Lean.Meta.Grind.GoalState

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 401c76f serving mathlib revision a3d2529