Loogle!

Result

Found 19 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 α)
• Std.Queue.mk.injEq 📋 Init.Data.Queue
  {α : Type u} (eList dList eList✝ dList✝ : List α) : ({ eList := eList, dList := dList } = { eList := eList✝, dList := dList✝ }) = (eList = eList✝ ∧ dList = dList✝)
• Std.Queue.mk.sizeOf_spec 📋 Init.Data.Queue
  {α : Type u} [SizeOf α] (eList dList : List α) : sizeOf { eList := eList, dList := dList } = 1 + sizeOf eList + sizeOf dList
• Lean.Meta.Grind.Goal.newRawFacts 📋 Lean.Meta.Tactic.Grind.Types
  (self : Lean.Meta.Grind.Goal) : Std.Queue Lean.Meta.Grind.NewRawFact
• Lean.Meta.Grind.Goal.mk 📋 Lean.Meta.Tactic.Grind.Types
  (mvarId : Lean.MVarId) (canon : Lean.Meta.Grind.Canon.State) (enodes : Lean.Meta.Grind.ENodeMap) (parents : Lean.Meta.Grind.ParentMap) (congrTable : Lean.Meta.Grind.CongrTable enodes) (appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (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.Grind.ENodeKey (Array Lean.Meta.Ext.ExtTheorem)) (ematch : Lean.Meta.Grind.EMatch.State) (split : Lean.Meta.Grind.Split.State) (arith : Lean.Meta.Grind.Arith.State) (clean : Lean.Meta.Grind.Clean.State) : Lean.Meta.Grind.Goal
• Lean.Meta.Grind.Goal.mk.injEq 📋 Lean.Meta.Tactic.Grind.Types
  (mvarId : Lean.MVarId) (canon : Lean.Meta.Grind.Canon.State) (enodes : Lean.Meta.Grind.ENodeMap) (parents : Lean.Meta.Grind.ParentMap) (congrTable : Lean.Meta.Grind.CongrTable enodes) (appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (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.Grind.ENodeKey (Array Lean.Meta.Ext.ExtTheorem)) (ematch : Lean.Meta.Grind.EMatch.State) (split : Lean.Meta.Grind.Split.State) (arith : Lean.Meta.Grind.Arith.State) (clean : Lean.Meta.Grind.Clean.State) (mvarId✝ : Lean.MVarId) (canon✝ : Lean.Meta.Grind.Canon.State) (enodes✝ : Lean.Meta.Grind.ENodeMap) (parents✝ : Lean.Meta.Grind.ParentMap) (congrTable✝ : Lean.Meta.Grind.CongrTable enodes✝) (appMap✝ : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (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.Grind.ENodeKey (Array Lean.Meta.Ext.ExtTheorem)) (ematch✝ : Lean.Meta.Grind.EMatch.State) (split✝ : Lean.Meta.Grind.Split.State) (arith✝ : Lean.Meta.Grind.Arith.State) (clean✝ : Lean.Meta.Grind.Clean.State) : ({ mvarId := mvarId, canon := canon, enodes := enodes, parents := parents, congrTable := congrTable, appMap := appMap, newFacts := newFacts, inconsistent := inconsistent, nextIdx := nextIdx, newRawFacts := newRawFacts, facts := facts, extThms := extThms, ematch := ematch, split := split, arith := arith, clean := clean } = { mvarId := mvarId✝, canon := canon✝, enodes := enodes✝, parents := parents✝, congrTable := congrTable✝, appMap := appMap✝, newFacts := newFacts✝, inconsistent := inconsistent✝, nextIdx := nextIdx✝, newRawFacts := newRawFacts✝, facts := facts✝, extThms := extThms✝, ematch := ematch✝, split := split✝, arith := arith✝, clean := clean✝ }) = (mvarId = mvarId✝ ∧ canon = canon✝ ∧ enodes = enodes✝ ∧ parents = parents✝ ∧ HEq congrTable congrTable✝ ∧ appMap = appMap✝ ∧ newFacts = newFacts✝ ∧ inconsistent = inconsistent✝ ∧ nextIdx = nextIdx✝ ∧ newRawFacts = newRawFacts✝ ∧ facts = facts✝ ∧ extThms = extThms✝ ∧ ematch = ematch✝ ∧ split = split✝ ∧ arith = arith✝ ∧ clean = clean✝)
• Lean.Meta.Grind.Goal.mk.sizeOf_spec 📋 Lean.Meta.Tactic.Grind.Types
  (mvarId : Lean.MVarId) (canon : Lean.Meta.Grind.Canon.State) (enodes : Lean.Meta.Grind.ENodeMap) (parents : Lean.Meta.Grind.ParentMap) (congrTable : Lean.Meta.Grind.CongrTable enodes) (appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (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.Grind.ENodeKey (Array Lean.Meta.Ext.ExtTheorem)) (ematch : Lean.Meta.Grind.EMatch.State) (split : Lean.Meta.Grind.Split.State) (arith : Lean.Meta.Grind.Arith.State) (clean : Lean.Meta.Grind.Clean.State) : sizeOf { mvarId := mvarId, canon := canon, enodes := enodes, parents := parents, congrTable := congrTable, appMap := appMap, newFacts := newFacts, inconsistent := inconsistent, nextIdx := nextIdx, newRawFacts := newRawFacts, facts := facts, extThms := extThms, ematch := ematch, split := split, arith := arith, clean := clean } = 1 + sizeOf mvarId + sizeOf canon + sizeOf enodes + sizeOf parents + sizeOf congrTable + sizeOf appMap + sizeOf newFacts + sizeOf inconsistent + sizeOf nextIdx + sizeOf newRawFacts + sizeOf facts + sizeOf extThms + sizeOf ematch + sizeOf split + sizeOf arith + sizeOf clean

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 19971e9 serving mathlib revision f167e8d