Loogle!

Result

Found 10766 definitions mentioning List. Of these, 170 match your pattern(s).

List.concat 📋 Init.Prelude
{α : Type u} : List α → α → List α
List.cons 📋 Init.Prelude
{α : Type u} (head : α) (tail : List α) : List α
List.set 📋 Init.Prelude
{α : Type u_1} : List α → ℕ → α → List α
List.dropLast 📋 Init.Data.List.Basic
{α : Type u_1} : List α → List α
List.reverse 📋 Init.Data.List.Basic
{α : Type u} (as : List α) : List α
List.tail 📋 Init.Data.List.Basic
{α : Type u} : List α → List α
List.drop 📋 Init.Data.List.Basic
{α : Type u} : ℕ → List α → List α
List.eraseIdx 📋 Init.Data.List.Basic
{α : Type u} : List α → ℕ → List α
List.intersperse 📋 Init.Data.List.Basic
{α : Type u} (sep : α) : List α → List α
List.intersperseTR 📋 Init.Data.List.Basic
{α : Type u} (sep : α) : List α → List α
List.take 📋 Init.Data.List.Basic
{α : Type u} : ℕ → List α → List α
List.append 📋 Init.Data.List.Basic
{α : Type u} (xs ys : List α) : List α
List.appendTR 📋 Init.Data.List.Basic
{α : Type u} (as bs : List α) : List α
List.dropWhile 📋 Init.Data.List.Basic
{α : Type u} (p : α → Bool) : List α → List α
List.eraseDups 📋 Init.Data.List.Basic
{α : Type u_1} [BEq α] (as : List α) : List α
List.eraseP 📋 Init.Data.List.Basic
{α : Type u} (p : α → Bool) : List α → List α
List.eraseReps 📋 Init.Data.List.Basic
{α : Type u_1} [BEq α] : List α → List α
List.filter 📋 Init.Data.List.Basic
{α : Type u} (p : α → Bool) : List α → List α
List.filterTR 📋 Init.Data.List.Basic
{α : Type u} (p : α → Bool) (as : List α) : List α
List.insertIdx 📋 Init.Data.List.Basic
{α : Type u} (n : ℕ) (a : α) : List α → List α
List.leftpad 📋 Init.Data.List.Basic
{α : Type u} (n : ℕ) (a : α) (l : List α) : List α
List.leftpadTR 📋 Init.Data.List.Basic
{α : Type u} (n : ℕ) (a : α) (l : List α) : List α
List.modifyHead 📋 Init.Data.List.Basic
{α : Type u} (f : α → α) : List α → List α
List.reverseAux 📋 Init.Data.List.Basic
{α : Type u} : List α → List α → List α
List.rightpad 📋 Init.Data.List.Basic
{α : Type u} (n : ℕ) (a : α) (l : List α) : List α
List.tailD 📋 Init.Data.List.Basic
{α : Type u} (list fallback : List α) : List α
List.takeWhile 📋 Init.Data.List.Basic
{α : Type u} (p : α → Bool) (xs : List α) : List α
List.replicateTR.loop 📋 Init.Data.List.Basic
{α : Type u} (a : α) : ℕ → List α → List α
List.erase 📋 Init.Data.List.Basic
{α : Type u_1} [BEq α] : List α → α → List α
List.insert 📋 Init.Data.List.Basic
{α : Type u} [BEq α] (a : α) (l : List α) : List α
List.intercalate 📋 Init.Data.List.Basic
{α : Type u} (sep : List α) (xs : List (List α)) : List α
List.modify 📋 Init.Data.List.Basic
{α : Type u} (f : α → α) : ℕ → List α → List α
List.intersperse_eq_intersperseTR 📋 Init.Data.List.Basic
: @List.intersperse = @List.intersperseTR
List.removeAll 📋 Init.Data.List.Basic
{α : Type u} [BEq α] (xs ys : List α) : List α
List.replace 📋 Init.Data.List.Basic
{α : Type u} [BEq α] : List α → α → α → List α
List.eraseDups.loop 📋 Init.Data.List.Basic
{α : Type u_1} [BEq α] : List α → List α → List α
List.filterTR.loop 📋 Init.Data.List.Basic
{α : Type u} (p : α → Bool) : List α → List α → List α
List.append_eq_appendTR 📋 Init.Data.List.Basic
: @List.append = @List.appendTR
List.filter_eq_filterTR 📋 Init.Data.List.Basic
: @List.filter = @List.filterTR
List.leftpad_eq_leftpadTR 📋 Init.Data.List.Basic
: @List.leftpad = @List.leftpadTR
List.modifyTailIdx 📋 Init.Data.List.Basic
{α : Type u} (f : List α → List α) : ℕ → List α → List α
List.eraseReps.loop 📋 Init.Data.List.Basic
{α : Type u_1} [BEq α] : α → List α → List α → List α
List.mapTR.loop 📋 Init.Data.List.Basic
{α : Type u} {β : Type v} (f : α → β) : List α → List β → List β
List.rotateLeft 📋 Init.Data.List.Basic
{α : Type u} (xs : List α) (n : ℕ := 1) : List α
List.rotateRight 📋 Init.Data.List.Basic
{α : Type u} (xs : List α) (n : ℕ := 1) : List α
List.splitBy.loop 📋 Init.Data.List.Basic
{α : Type u} (R : α → α → Bool) : List α → α → List α → List (List α) → List (List α)
ReprTuple.reprTuple 📋 Init.Data.Repr
{α : Type u} [self : ReprTuple α] : α → List Lean.Format → List Lean.Format
Array.toListAppend 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (l : List α) : List α
Array.toListLitAux 📋 Init.Data.Array.GetLit
{α : Type u_1} (a : Array α) (n : ℕ) (hsz : a.size = n) (i : ℕ) : i ≤ a.size → List α → List α
List.tail! 📋 Init.Data.List.BasicAux
{α : Type u_1} : List α → List α
List.mapMono 📋 Init.Data.List.BasicAux
{α : Type u_1} (as : List α) (f : α → α) : List α
List.dropLastTR 📋 Init.Data.List.Impl
{α : Type u_1} (l : List α) : List α
List.eraseIdxTR 📋 Init.Data.List.Impl
{α : Type u_1} (l : List α) (n : ℕ) : List α
List.takeTR 📋 Init.Data.List.Impl
{α : Type u_1} (n : ℕ) (l : List α) : List α
List.erasePTR 📋 Init.Data.List.Impl
{α : Type u_1} (p : α → Bool) (l : List α) : List α
List.insertIdxTR 📋 Init.Data.List.Impl
{α : Type u_1} (n : ℕ) (a : α) (l : List α) : List α
List.setTR 📋 Init.Data.List.Impl
{α : Type u_1} (l : List α) (n : ℕ) (a : α) : List α
List.takeWhileTR 📋 Init.Data.List.Impl
{α : Type u_1} (p : α → Bool) (l : List α) : List α
List.dropLast_eq_dropLastTR 📋 Init.Data.List.Impl
: @List.dropLast = @List.dropLastTR
List.eraseTR 📋 Init.Data.List.Impl
{α : Type u_1} [BEq α] (l : List α) (a : α) : List α
List.intercalateTR 📋 Init.Data.List.Impl
{α : Type u_1} (sep : List α) : List (List α) → List α
List.modifyTR 📋 Init.Data.List.Impl
{α : Type u_1} (f : α → α) (n : ℕ) (l : List α) : List α
List.eraseIdx_eq_eraseIdxTR 📋 Init.Data.List.Impl
: @List.eraseIdx = @List.eraseIdxTR
List.replaceTR 📋 Init.Data.List.Impl
{α : Type u_1} [BEq α] (l : List α) (b c : α) : List α
List.take_eq_takeTR 📋 Init.Data.List.Impl
: @List.take = @List.takeTR
List.insertIdxTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (a : α) : ℕ → List α → Array α → List α
List.eraseP_eq_erasePTR 📋 Init.Data.List.Impl
: @List.eraseP = @List.erasePTR
List.insertIdx_eq_insertIdxTR 📋 Init.Data.List.Impl
: @List.insertIdx = @List.insertIdxTR
List.set_eq_setTR 📋 Init.Data.List.Impl
: @List.set = @List.setTR
List.takeWhile_eq_takeWhileTR 📋 Init.Data.List.Impl
: @List.takeWhile = @List.takeWhileTR
List.eraseIdxTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (l : List α) : List α → ℕ → Array α → List α
List.modifyTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (f : α → α) : List α → ℕ → Array α → List α
List.takeTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (l : List α) : List α → ℕ → Array α → List α
List.erase_eq_eraseTR 📋 Init.Data.List.Impl
: @List.erase = @List.eraseTR
List.intercalate_eq_intercalateTR 📋 Init.Data.List.Impl
: @List.intercalate = @List.intercalateTR
List.modify_eq_modifyTR 📋 Init.Data.List.Impl
: @List.modify = @List.modifyTR
List.erasePTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (p : α → Bool) (l : List α) : List α → Array α → List α
List.setTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (l : List α) (a : α) : List α → ℕ → Array α → List α
List.takeWhileTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (p : α → Bool) (l : List α) : List α → Array α → List α
List.replace_eq_replaceTR 📋 Init.Data.List.Impl
: @List.replace = @List.replaceTR
List.eraseTR.go 📋 Init.Data.List.Impl
{α : Type u_1} [BEq α] (l : List α) (a : α) : List α → Array α → List α
List.intercalateTR.go 📋 Init.Data.List.Impl
{α : Type u_1} (sep : Array α) : List α → List (List α) → Array α → List α
List.replaceTR.go 📋 Init.Data.List.Impl
{α : Type u_1} [BEq α] (l : List α) (b c : α) : List α → Array α → List α
List.mergeSort 📋 Init.Data.List.Sort.Basic
{α : Type u_1} (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α
List.merge 📋 Init.Data.List.Sort.Basic
{α : Type u_1} (xs ys : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α
List.MergeSort.Internal.mergeSortTR 📋 Init.Data.List.Sort.Impl
{α : Type u_1} (l : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α
List.MergeSort.Internal.mergeSortTR₂ 📋 Init.Data.List.Sort.Impl
{α : Type u_1} (l : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α
List.MergeSort.Internal.mergeTR 📋 Init.Data.List.Sort.Impl
{α : Type u_1} (l₁ l₂ : List α) (le : α → α → Bool) : List α
List.MergeSort.Internal.mergeTR.go 📋 Init.Data.List.Sort.Impl
{α : Type u_1} (le : α → α → Bool) : List α → List α → List α → List α
List.MergeSort.Internal.mergeSort_eq_mergeSortTR 📋 Init.Data.List.Sort.Impl
: @List.mergeSort = @List.MergeSort.Internal.mergeSortTR
List.MergeSort.Internal.mergeSort_eq_mergeSortTR₂ 📋 Init.Data.List.Sort.Impl
: @List.mergeSort = @List.MergeSort.Internal.mergeSortTR₂
List.MergeSort.Internal.merge_eq_mergeTR 📋 Init.Data.List.Sort.Impl
: @List.merge = @List.MergeSort.Internal.mergeTR
Lean.Data.AC.removeNeutrals 📋 Init.Data.AC
{α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α) : List ℕ → List ℕ
Lean.Data.AC.removeNeutrals.loop 📋 Init.Data.AC
{α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α) : List ℕ → List ℕ
Std.DHashMap.Internal.List.eraseKey 📋 Std.Data.DHashMap.Internal.List.Associative
{α : Type u} {β : α → Type v} [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) × β a)
Std.DHashMap.Internal.List.insertEntry 📋 Std.Data.DHashMap.Internal.List.Associative
{α : Type u} {β : α → Type v} [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) : List ((a : α) × β a)
Std.DHashMap.Internal.List.insertEntryIfNew 📋 Std.Data.DHashMap.Internal.List.Associative
{α : Type u} {β : α → Type v} [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) : List ((a : α) × β a)
Std.DHashMap.Internal.List.replaceEntry 📋 Std.Data.DHashMap.Internal.List.Associative
{α : Type u} {β : α → Type v} [BEq α] (k : α) (v : β k) : List ((a : α) × β a) → List ((a : α) × β a)
List.rotate 📋 Batteries.Data.List.Basic
{α : Type u_1} (l : List α) (n : ℕ) : List α
List.rotate' 📋 Batteries.Data.List.Basic
{α : Type u_1} : List α → ℕ → List α
List.after 📋 Batteries.Data.List.Basic
{α : Type u_1} (p : α → Bool) : List α → List α
List.dropSlice 📋 Batteries.Data.List.Basic
{α : Type u_1} : ℕ → ℕ → List α → List α
List.dropSliceTR 📋 Batteries.Data.List.Basic
{α : Type u_1} (n m : ℕ) (l : List α) : List α
List.eraseDup 📋 Batteries.Data.List.Basic
{α : Type u_1} [BEq α] : List α → List α
List.insertNth 📋 Batteries.Data.List.Basic
{α : Type u} (n : ℕ) (a : α) : List α → List α
List.modifyLast 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → α) (l : List α) : List α
List.sections 📋 Batteries.Data.List.Basic
{α : Type u_1} : List (List α) → List (List α)
List.sectionsTR 📋 Batteries.Data.List.Basic
{α : Type u_1} (L : List (List α)) : List (List α)
List.takeD 📋 Batteries.Data.List.Basic
{α : Type u_1} : ℕ → List α → α → List α
List.takeDTR 📋 Batteries.Data.List.Basic
{α : Type u_1} (n : ℕ) (l : List α) (dflt : α) : List α
List.transpose 📋 Batteries.Data.List.Basic
{α : Type u_1} (l : List (List α)) : List (List α)
List.fillNones 📋 Batteries.Data.List.Basic
{α : Type u_1} : List (Option α) → List α → List α
List.fillNonesTR 📋 Batteries.Data.List.Basic
{α : Type u_1} (as : List (Option α)) (as' : List α) : List α
List.insertP 📋 Batteries.Data.List.Basic
{α : Type u_1} (p : α → Bool) (a : α) (l : List α) : List α
List.lookmap 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → Option α) (l : List α) : List α
List.modifyNth 📋 Batteries.Data.List.Basic
{α : Type u} (f : α → α) : ℕ → List α → List α
List.replaceF 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → Option α) : List α → List α
List.replaceFTR 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → Option α) (l : List α) : List α
List.bagInter 📋 Batteries.Data.List.Basic
{α : Type u_1} [BEq α] : List α → List α → List α
List.diff 📋 Batteries.Data.List.Basic
{α : Type u_1} [BEq α] : List α → List α → List α
List.inter 📋 Batteries.Data.List.Basic
{α : Type u_1} [BEq α] (l₁ l₂ : List α) : List α
List.union 📋 Batteries.Data.List.Basic
{α : Type u_1} [BEq α] (l₁ l₂ : List α) : List α
List.modifyLast.go 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → α) : List α → Array α → List α
List.takeDTR.go 📋 Batteries.Data.List.Basic
{α : Type u_1} (dflt : α) : ℕ → List α → Array α → List α
List.dropSlice_eq_dropSliceTR 📋 Batteries.Data.List.Basic
: @List.dropSlice = @List.dropSliceTR
List.modifyNthTail 📋 Batteries.Data.List.Basic
{α : Type u} (f : List α → List α) : ℕ → List α → List α
List.sections_eq_sectionsTR 📋 Batteries.Data.List.Basic
: @List.sections = @List.sectionsTR
List.takeD_eq_takeDTR 📋 Batteries.Data.List.Basic
: @List.takeD = @List.takeDTR
List.fillNonesTR.go 📋 Batteries.Data.List.Basic
{α : Type u_1} : List (Option α) → List α → Array α → List α
List.insertP.loop 📋 Batteries.Data.List.Basic
{α : Type u_1} (p : α → Bool) (a : α) : List α → List α → List α
List.lookmap.go 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → Option α) : List α → Array α → List α
List.replaceFTR.go 📋 Batteries.Data.List.Basic
{α : Type u_1} (f : α → Option α) : List α → Array α → List α
List.fillNones_eq_fillNonesTR 📋 Batteries.Data.List.Basic
: @List.fillNones = @List.fillNonesTR
List.pwFilter 📋 Batteries.Data.List.Basic
{α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) : List α
List.replaceF_eq_replaceFTR 📋 Batteries.Data.List.Basic
: @List.replaceF = @List.replaceFTR
List.dropSliceTR.go 📋 Batteries.Data.List.Basic
{α : Type u_1} (l : List α) (m : ℕ) : List α → ℕ → Array α → List α
Batteries.DList.apply 📋 Batteries.Data.DList.Basic
{α : Type u} (self : Batteries.DList α) : List α → List α
Batteries.RBNode.Path.withList 📋 Batteries.Data.RBMap.Lemmas
{α : Type u_1} (p : Batteries.RBNode.Path α) (l : List α) : List α
List.swapFirstTwo 📋 Mathlib.Tactic.ToAdditive.Frontend
{α : Type u_1} : List α → List α
Mathlib.Tactic.MkIff.List.init 📋 Mathlib.Tactic.MkIffOfInductiveProp
{α : Type u_1} : List α → List α
Plausible.TotalFunction.shrink.dedup 📋 Plausible.Functions
{α : Type u_1} {β : Type u_2} [DecidableEq α] (m' : List ((_ : α) × β)) : List ((_ : α) × β)
Plausible.TotalFunction.shrink.dedup.insertKey 📋 Plausible.Functions
{α : Type u_1} {β : Type u_2} [DecidableEq α] (xs : List ((_ : α) × β)) (pair : (_ : α) × β) : List ((_ : α) × β)
List.dedup 📋 Mathlib.Data.List.Defs
{α : Type u_1} [DecidableEq α] : List α → List α
List.takeI 📋 Mathlib.Data.List.Defs
{α : Type u_1} [Inhabited α] (n : ℕ) (l : List α) : List α
List.replaceIf 📋 Mathlib.Data.List.Defs
{α : Type u_1} : List α → List Bool → List α → List α
List.iterateTR.loop 📋 Mathlib.Data.List.Defs
{α : Type u_1} (f : α → α) (a : α) (n : ℕ) (l : List α) : List α
List.destutter 📋 Mathlib.Data.List.Defs
{α : Type u_1} (R : α → α → Prop) [DecidableRel R] : List α → List α
List.destutter' 📋 Mathlib.Data.List.Defs
{α : Type u_1} (R : α → α → Prop) [DecidableRel R] : α → List α → List α
List.sublistsAux 📋 Mathlib.Data.List.Sublists
{α : Type u} (a : α) (r : List (List α)) : List (List α)
List.sublists'Aux 📋 Mathlib.Data.List.Sublists
{α : Type u} (a : α) (r₁ r₂ : List (List α)) : List (List α)
List.sublistsLenAux 📋 Mathlib.Data.List.Sublists
{α : Type u} {β : Type v} : ℕ → List α → (List α → β) → List β → List β
List.insertionSort 📋 Mathlib.Data.List.Sort
{α : Type u} (r : α → α → Prop) [DecidableRel r] : List α → List α
List.orderedInsert 📋 Mathlib.Data.List.Sort
{α : Type u} (r : α → α → Prop) [DecidableRel r] (a : α) : List α → List α
FreeAddGroup.negRev 📋 Mathlib.GroupTheory.FreeGroup.Basic
{α : Type u} (w : List (α × Bool)) : List (α × Bool)
FreeGroup.invRev 📋 Mathlib.GroupTheory.FreeGroup.Basic
{α : Type u} (w : List (α × Bool)) : List (α × Bool)
FreeAddGroup.reduce 📋 Mathlib.GroupTheory.FreeGroup.Reduce
{α : Type u_1} [DecidableEq α] (L : List (α × Bool)) : List (α × Bool)
FreeGroup.reduce 📋 Mathlib.GroupTheory.FreeGroup.Reduce
{α : Type u_1} [DecidableEq α] (L : List (α × Bool)) : List (α × Bool)
Mathlib.MoveAdd.reorderUsing 📋 Mathlib.Tactic.MoveAdd
{α : Type u_1} [BEq α] (toReorder : List α) (instructions : List (α × Bool)) : List α
Turing.TM2to1.stWrite 📋 Mathlib.Computability.TuringMachine
{K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) : Turing.TM2to1.StAct k → List (Γ k)
List.dedupKeys 📋 Mathlib.Data.List.Sigma
{α : Type u} {β : α → Type v} [DecidableEq α] : List (Sigma β) → List (Sigma β)
List.kerase 📋 Mathlib.Data.List.Sigma
{α : Type u} {β : α → Type v} [DecidableEq α] (a : α) : List (Sigma β) → List (Sigma β)
List.kinsert 📋 Mathlib.Data.List.Sigma
{α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) : List (Sigma β)
List.kreplace 📋 Mathlib.Data.List.Sigma
{α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) : List (Sigma β) → List (Sigma β)
List.kunion 📋 Mathlib.Data.List.Sigma
{α : Type u} {β : α → Type v} [DecidableEq α] : List (Sigma β) → List (Sigma β) → List (Sigma β)
List.rdrop 📋 Mathlib.Data.List.DropRight
{α : Type u_1} (l : List α) (n : ℕ) : List α
List.rtake 📋 Mathlib.Data.List.DropRight
{α : Type u_1} (l : List α) (n : ℕ) : List α
List.rdropWhile 📋 Mathlib.Data.List.DropRight
{α : Type u_1} (p : α → Bool) (l : List α) : List α
List.rtakeWhile 📋 Mathlib.Data.List.DropRight
{α : Type u_1} (p : α → Bool) (l : List α) : List α
LevenshteinEstimator'.pre_rev 📋 Mathlib.Data.List.EditDistance.Estimator
{α : Type u_1} {β δ : Type} [CanonicallyLinearOrderedAddCommMonoid δ] {C : Levenshtein.Cost α β δ} {xs : List α} {ys : List β} (self : LevenshteinEstimator' C xs ys) : List β
LevenshteinEstimator'.suff 📋 Mathlib.Data.List.EditDistance.Estimator
{α : Type u_1} {β δ : Type} [CanonicallyLinearOrderedAddCommMonoid δ] {C : Levenshtein.Cost α β δ} {xs : List α} {ys : List β} (self : LevenshteinEstimator' C xs ys) : List β

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 ?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
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, _ * _, _ ^ _, |- _ < _ → _
woould 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 026c9d9 serving mathlib revision 0e2973b