Loogle!

Result

Found 21 declarations mentioning Std.Iter.map.

• Std.Iter.map 📋 Init.Data.Iterators.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] (f : β → γ) (it : Std.Iter β) : Std.Iter γ
• Std.Iter.toArray_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → γ} : (Std.Iter.map f it).toArray = Array.map f it.toArray
• Std.Iter.toListRev_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → γ} : (Std.Iter.map f it).toListRev = List.map f it.toListRev
• Std.Iter.toList_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → γ} : (Std.Iter.map f it).toList = List.map f it.toList
• Std.Iter.map_eq_toIter_map_toIterM 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] {it : Std.Iter β} {f : β → γ} : Std.Iter.map f it = (Std.IterM.map f it.toIterM).toIter
• Std.Iter.map.eq_1 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] (f : β → γ) (it : Std.Iter β) : Std.Iter.map f it = (Std.IterM.map f it.toIterM).toIter
• Std.Iter.count_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β β' : Type w} [Std.Iterator α Id β] [Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'} : (Std.Iter.map f it).count = it.count
• Std.Iter.all_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β β' : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'} {p : β' → Bool} : Std.Iter.all p (Std.Iter.map f it) = Std.Iter.all (fun x => p (f x)) it
• Std.Iter.any_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β β' : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'} {p : β' → Bool} : Std.Iter.any p (Std.Iter.map f it) = Std.Iter.any (fun x => p (f x)) it
• Std.Iter.fold_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ δ : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {f : β → γ} {g : δ → γ → δ} {init : δ} {it : Std.Iter β} : Std.Iter.fold g init (Std.Iter.map f it) = Std.Iter.fold (fun d b => g d (f b)) init it
• Std.Iter.allM_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β β' : Type w} {m : Type → Type w'} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Monad m] [Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → β'} {p : β' → m Bool} : Std.Iter.allM p (Std.Iter.map f it) = Std.Iter.allM (fun x => p (f x)) it
• Std.Iter.anyM_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β β' : Type w} {m : Type → Type w'} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Monad m] [Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → β'} {p : β' → m Bool} : Std.Iter.anyM p (Std.Iter.map f it) = Std.Iter.anyM (fun x => p (f x)) it
• Std.Iter.foldM_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ δ : Type w} {n : Type w → Type w''} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Std.Iter β} : Std.Iter.foldM g init (Std.Iter.map f it) = Std.Iter.foldM (fun d b => g d (f b)) init it
• Std.Iter.forIn_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] {n : Type w → Type w''} {β₂ : Type w} [Monad n] [LawfulMonad n] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} : forIn (Std.Iter.map f it) init g = forIn it init fun out acc => g (f out) acc
• Std.Iter.step_map 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterator α Id β] {it : Std.Iter β} {f : β → γ} : (Std.Iter.map f it).step = match it.step with | ⟨Std.IterStep.yield it' out, h⟩ => Std.PlausibleIterStep.yield (Std.Iter.map f it') (f out) ⋯ | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.map f it') ⋯ | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
• Std.Iter.toArray_flatMap 📋 Init.Data.Iterators.Lemmas.Combinators.FlatMap
  {α α₂ β γ : Type w} [Std.Iterator α Id β] [Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id] [Std.Iterators.Finite α₂ Id] [Std.Iterator α Id β] [Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id] [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β} : (Std.Iter.flatMap f it₁).toArray = (Std.Iter.map (fun b => (f b).toArray) it₁).toArray.flatten
• Std.Iter.toList_flatMap 📋 Init.Data.Iterators.Lemmas.Combinators.FlatMap
  {α α₂ β γ : Type w} [Std.Iterator α Id β] [Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id] [Std.Iterators.Finite α₂ Id] [Std.Iterator α Id β] [Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id] [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β} : (Std.Iter.flatMap f it₁).toList = (Std.Iter.map (fun b => (f b).toList) it₁).toList.flatten
• Std.Iter.toArray_flatMapAfter 📋 Init.Data.Iterators.Lemmas.Combinators.FlatMap
  {α α₂ β γ : Type w} [Std.Iterator α Id β] [Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id] [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β} {it₂ : Option (Std.Iter γ)} : (Std.Iter.flatMapAfter f it₁ it₂).toArray = match it₂ with | none => (Std.Iter.map (fun b => (f b).toArray) it₁).toArray.flatten | some it₂ => it₂.toArray ++ (Std.Iter.map (fun b => (f b).toArray) it₁).toArray.flatten
• Std.Iter.toList_flatMapAfter 📋 Init.Data.Iterators.Lemmas.Combinators.FlatMap
  {α α₂ β γ : Type w} [Std.Iterator α Id β] [Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id] [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β} {it₂ : Option (Std.Iter γ)} : (Std.Iter.flatMapAfter f it₁ it₂).toList = match it₂ with | none => (Std.Iter.map (fun b => (f b).toList) it₁).toList.flatten | some it₂ => it₂.toList ++ (Std.Iter.map (fun b => (f b).toList) it₁).toList.flatten
• Std.Do.Iter.foldM_map 📋 Std.Do.Triple.SpecLemmas
  {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Std.Do.WPMonad n ps] [Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps} (h : ⦃P⦄ Std.Iter.foldM (fun d b => g d (f b)) init it ⦃Q⦄) : ⦃P⦄ Std.Iter.foldM g init (Std.Iter.map f it) ⦃Q⦄
• Std.Do.Spec.Iter.forIn_map 📋 Std.Do.Triple.SpecLemmas
  {α β β₂ γ : Type w} [Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1} [Monad n] [LawfulMonad n] [Std.Do.WPMonad n ps] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps} (h : ⦃P⦄ forIn it init fun out acc => g (f out) acc ⦃Q⦄) : ⦃P⦄ forIn (Std.Iter.map f it) init g ⦃Q⦄

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 36960b0 serving mathlib revision 9a4cf1d