Loogle!
Result
Found 34 declarations mentioning Std.DHashMap.Internal.Raw₀.getD.
- Std.DHashMap.Internal.Raw₀.getD 📋 Std.Data.DHashMap.Internal.Defs
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) : β a - Std.DHashMap.Internal.Raw.getD_eq 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {fallback : β a} : m.getD a fallback = Std.DHashMap.Internal.Raw₀.getD ⟨m, ⋯⟩ a fallback - Std.DHashMap.Raw.getD.eq_1 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : m.getD a fallback = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.getD ⟨m, h⟩ a fallback else fallback - Std.DHashMap.Internal.Raw₀.getD_eq_getDₘ 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) : m.getD a fallback = m.getDₘ a fallback - Std.DHashMap.Internal.Raw₀.getD.eq_1 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (a : α) (fallback : β a) (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size) : Std.DHashMap.Internal.Raw₀.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback = Std.DHashMap.Internal.AssocList.getCastD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))] - Std.DHashMap.Internal.Raw₀.getD_eq_getValueCastD 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {fallback : β a} : m.getD a fallback = Std.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback - Std.DHashMap.Internal.Raw₀.getD_empty 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {fallback : β a} {c : ℕ} : (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_emptyWithCapacity 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {fallback : β a} {c : ℕ} : (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_erase_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k : α} {fallback : β k} : (m.erase k).getD k fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_insert_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback b : β a} : (m.insert a b).getD a fallback = b - Std.DHashMap.Internal.Raw₀.getD_eq_fallback 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : m.contains a = false → m.getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_eq_getD_get? 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : m.getD a fallback = (m.get? a).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = m.getD a fallback - Std.DHashMap.Internal.Raw₀.get!_eq_getD_default 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} [Inhabited (β a)] : m.get! a = m.getD a default - Std.DHashMap.Internal.Raw₀.get_eq_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} {h✝ : m.contains a = true} : m.get a h✝ = m.getD a fallback - Std.DHashMap.Internal.Raw₀.get?_eq_some_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : m.contains a = true → m.get? a = some (m.getD a fallback) - Std.DHashMap.Internal.Raw₀.getD_filter 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_alter_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k : α} {fallback : β k} (h : (↑m).WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_modify_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k : α} {fallback : β k} {f : β k → β k} : (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_of_isEmpty 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : (↑m).isEmpty = true → m.getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_filterMap 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_erase 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k a : α} {fallback : β a} : (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback - Std.DHashMap.Internal.Raw₀.getD_insert 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k a : α} {fallback : β a} {v : β k} : (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback - Std.DHashMap.Internal.Raw₀.getD_eq_of_equiv 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β) [LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) (h : (↑m₁).Equiv ↑m₂) {k : α} {fallback : β k} : m₁.getD k fallback = m₂.getD k fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_alter 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k k' : α} {fallback : β k'} (h : (↑m).WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback - Std.DHashMap.Internal.Raw₀.getD_modify 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k k' : α} {fallback : β k'} {f : β k → β k} : (m.modify k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(m.insertMany l)).getD k fallback = m.getD k fallback - Std.DHashMap.Internal.Raw₀.getD_insertIfNew 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k a : α} {fallback : β a} {v : β k} : (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k' fallback = cast ⋯ v - Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k' fallback = cast ⋯ v - Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (↑(m.insertMany l)).getD k' fallback = cast ⋯ v
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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 bce1d65