Loogle!
Result
Found 34 declarations mentioning Std.DHashMap.Internal.Raw₀.map.
- Std.DHashMap.Internal.Raw₀.map 📋 Std.Data.DHashMap.Internal.Defs
{α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (m : Std.DHashMap.Internal.Raw₀ α β) : Std.DHashMap.Internal.Raw₀ α γ - Std.DHashMap.Internal.Raw.map_eq 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} : Std.DHashMap.Raw.map f m = ↑(Std.DHashMap.Internal.Raw₀.map f ⟨m, ⋯⟩) - Std.DHashMap.Raw.map.eq_1 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (m : Std.DHashMap.Raw α β) : Std.DHashMap.Raw.map f m = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.map f ⟨m, h⟩) else ∅ - Std.DHashMap.Internal.Raw₀.map_eq_mapₘ 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} {δ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → δ a) : Std.DHashMap.Internal.Raw₀.map f m = m.mapₘ f - Std.DHashMap.Internal.Raw₀.filterMap_eq_map 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → γ a) (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.filterMap (fun k v => some (f k v)) m = Std.DHashMap.Internal.Raw₀.map f m - Std.DHashMap.Internal.Raw₀.wf_map₀ 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (h : (↑m).WF) {f : (a : α) → β a → δ a} : (↑(Std.DHashMap.Internal.Raw₀.map f m)).WF - Std.DHashMap.Internal.Raw₀.wfImp_map 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a} (h : Std.DHashMap.Internal.Raw.WFImp ↑m) : Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.map f m) - Std.DHashMap.Internal.Raw₀.toListModel_map 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} {δ : α → Type w} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a} : (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.map f m)).buckets).Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (Std.DHashMap.Internal.toListModel (↑m).buckets)) - Std.DHashMap.Internal.Raw₀.map_id_equiv 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) : (↑(Std.DHashMap.Internal.Raw₀.map (fun x v => v) m)).Equiv ↑m - Std.DHashMap.Internal.Raw₀.keys_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → γ a} : (↑(Std.DHashMap.Internal.Raw₀.map f m)).keys.Perm (↑m).keys - Std.DHashMap.Internal.Raw₀.contains_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).contains k = m.contains k - Std.DHashMap.Internal.Raw₀.getKey?_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).getKey? k = m.getKey? k - Std.DHashMap.Internal.Raw₀.getKeyD_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k fallback : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).getKeyD k fallback = m.getKeyD k fallback - Std.DHashMap.Internal.Raw₀.contains_of_contains_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true → m.contains k = true - Std.DHashMap.Internal.Raw₀.getKey!_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).getKey! k = m.getKey! k - Std.DHashMap.Internal.Raw₀.get?_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 : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).get? k = Option.map (f k) (m.get? k) - 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₀.get!_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 : α} [Inhabited (γ k)] (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).get! k = (Option.map (f k) (m.get? k)).get! - Std.DHashMap.Internal.Raw₀.map_map_equiv 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} {γ : α → Type w} {δ : α → Type w'} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a} : (↑(Std.DHashMap.Internal.Raw₀.map g (Std.DHashMap.Internal.Raw₀.map f m))).Equiv ↑(Std.DHashMap.Internal.Raw₀.map (fun k v => g k (f k v)) m) - Std.DHashMap.Internal.Raw₀.Const.get?_map_of_getKey?_eq_some 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α} (h : (↑m).WF) : m.getKey? k = some k' → Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.map f m) k = Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k) - Std.DHashMap.Internal.Raw₀.getKey_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF) {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true} : (Std.DHashMap.Internal.Raw₀.map f m).getKey k h' = m.getKey k ⋯ - Std.DHashMap.Internal.Raw₀.Const.getD_map_of_getKey?_eq_some 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α} {fallback : γ} (h : (↑m).WF) : m.getKey? k = some k' → Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback = (Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback - Std.DHashMap.Internal.Raw₀.Const.get!_map_of_getKey?_eq_some 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} (h : (↑m).WF) : m.getKey? k = some k' → Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.map f m) k = (Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get! - Std.DHashMap.Internal.Raw₀.Const.toList_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{β : Type v} {γ : Type w} {α : Type u} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : α → β → γ} : (Std.DHashMap.Raw.Const.toList ↑(Std.DHashMap.Internal.Raw₀.map f m)).Perm (List.map (fun p => (p.1, f p.1 p.2)) (Std.DHashMap.Raw.Const.toList ↑m)) - Std.DHashMap.Internal.Raw₀.get_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 : α} (h : (↑m).WF) {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true} : (Std.DHashMap.Internal.Raw₀.map f m).get k h' = f k (m.get k ⋯) - Std.DHashMap.Internal.Raw₀.isEmpty_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} (h : (↑m).WF) : (↑(Std.DHashMap.Internal.Raw₀.map f m)).isEmpty = (↑m).isEmpty - Std.DHashMap.Internal.Raw₀.size_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} (h : (↑m).WF) : (↑(Std.DHashMap.Internal.Raw₀.map f m)).size = (↑m).size - Std.DHashMap.Internal.Raw₀.toList_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → γ a} : (↑(Std.DHashMap.Internal.Raw₀.map f m)).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (↑m).toList) - Std.DHashMap.Internal.Raw₀.filterMap_equiv_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} (h : (↑m).WF) : (↑(Std.DHashMap.Internal.Raw₀.filterMap (fun k v => some (f k v)) m)).Equiv ↑(Std.DHashMap.Internal.Raw₀.map f m) - Std.DHashMap.Internal.Raw₀.map_equiv_congr 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} {γ : α → Type w} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β) (h : (↑m₁).Equiv ↑m₂) {f : (a : α) → β a → γ a} : (↑(Std.DHashMap.Internal.Raw₀.map f m₁)).Equiv ↑(Std.DHashMap.Internal.Raw₀.map f m₂) - Std.DHashMap.Internal.Raw₀.Const.get_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} (h : (↑m).WF) {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true} : Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.map f m) k h' = f (m.getKey k ⋯) (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯) - Std.DHashMap.Internal.Raw₀.Const.get?_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.map f m) k = Option.pmap (fun v h' => f (m.getKey k h') v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯ - Std.DHashMap.Internal.Raw₀.Const.getD_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯).getD fallback - Std.DHashMap.Internal.Raw₀.Const.get!_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k : α} (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.map f m) k = (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯).get!
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