Loogle!
Result
Found 8096 definitions mentioning List. Of these, 155 match your pattern(s).
- List.concat Init.Prelude
{α : Type u} → List α → α → List α - List.cons Init.Prelude
{α : Type u} → α → 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} → 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} → α → List α → List α - List.take Init.Data.List.Basic
{α : Type u} → ℕ → List α → List α - List.append Init.Data.List.Basic
{α : Type u} → List α → List α → List α - List.appendTR Init.Data.List.Basic
{α : Type u} → List α → List α → List α - List.dropWhile Init.Data.List.Basic
{α : Type u} → (α → Bool) → List α → List α - List.eraseDups Init.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α - List.eraseReps Init.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α - List.filter Init.Data.List.Basic
{α : Type u} → (α → Bool) → List α → List α - List.filterTR Init.Data.List.Basic
{α : Type u} → (α → Bool) → List α → List α - List.reverseAux Init.Data.List.Basic
{α : Type u} → List α → List α → List α - List.takeWhile Init.Data.List.Basic
{α : Type u} → (α → Bool) → List α → List α - List.replicateTR.loop Init.Data.List.Basic
{α : Type u} → α → ℕ → List α → List α - List.erase Init.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → α → List α - List.insert Init.Data.List.Basic
{α : Type u} → [inst : BEq α] → α → List α → List α - List.intercalate Init.Data.List.Basic
{α : Type u} → List α → List (List α) → List α - List.removeAll Init.Data.List.Basic
{α : Type u} → [inst : BEq α] → List α → List α → List α - List.replace Init.Data.List.Basic
{α : Type u} → [inst : BEq α] → List α → α → α → List α - List.eraseDups.loop Init.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α → List α - List.filterTR.loop Init.Data.List.Basic
{α : Type u} → (α → 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.eraseReps.loop Init.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → α → List α → List α → List α - List.mapTR.loop Init.Data.List.Basic
{α : Type u} → {β : Type v} → (α → β) → List α → List β → List β - List.groupBy.loop Init.Data.List.Basic
{α : Type u} → (α → α → 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} → Array α → List α → List α - Array.toListLitAux Init.Data.Array.Basic
{α : Type u_1} → (a : Array α) → (n : ℕ) → 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} → List α → (α → α) → List α - List.tailD Init.Data.List.BasicAux
{α : Type u_1} → List α → List α → List α - List.rotateLeft Init.Data.List.BasicAux
{α : Type u_1} → List α → optParam ℕ 1 → List α - List.rotateRight Init.Data.List.BasicAux
{α : Type u_1} → List α → optParam ℕ 1 → List α - List.dropLastTR Init.Data.List.Impl
{α : Type u_1} → List α → List α - List.eraseIdxTR Init.Data.List.Impl
{α : Type u_1} → List α → ℕ → List α - List.intersperseTR Init.Data.List.Impl
{α : Type u_1} → α → List α → List α - List.takeTR Init.Data.List.Impl
{α : Type u_1} → ℕ → List α → List α - List.setTR Init.Data.List.Impl
{α : Type u_1} → List α → ℕ → α → List α - List.takeWhileTR Init.Data.List.Impl
{α : Type u_1} → (α → Bool) → List α → List α - List.dropLast_eq_dropLastTR Init.Data.List.Impl
@List.dropLast = @List.dropLastTR - List.eraseTR Init.Data.List.Impl
{α : Type u_1} → [inst : BEq α] → List α → α → List α - List.intercalateTR Init.Data.List.Impl
{α : Type u_1} → List α → List (List α) → List α - List.eraseIdx_eq_eraseIdxTR Init.Data.List.Impl
@List.eraseIdx = @List.eraseIdxTR - List.intersperse_eq_intersperseTR Init.Data.List.Impl
@List.intersperse = @List.intersperseTR - List.replaceTR Init.Data.List.Impl
{α : Type u_1} → [inst : BEq α] → List α → α → α → List α - List.take_eq_takeTR Init.Data.List.Impl
@List.take = @List.takeTR - 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} → List α → List α → ℕ → Array α → List α - List.takeTR.go Init.Data.List.Impl
{α : Type u_1} → 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.setTR.go Init.Data.List.Impl
{α : Type u_1} → List α → α → List α → ℕ → Array α → List α - List.takeWhileTR.go Init.Data.List.Impl
{α : Type u_1} → (α → Bool) → 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} → [inst : BEq α] → List α → α → List α → Array α → List α - List.intercalateTR.go Init.Data.List.Impl
{α : Type u_1} → Array α → List α → List (List α) → Array α → List α - List.replaceTR.go Init.Data.List.Impl
{α : Type u_1} → [inst : BEq α] → List α → α → α → List α → Array α → List α - Lean.Data.AC.removeNeutrals Init.Data.AC
{α : Sort u_1} → [info : Lean.Data.AC.ContextInformation α] → α → List ℕ → List ℕ - Lean.Data.AC.removeNeutrals.loop Init.Data.AC
{α : Sort u_1} → [info : Lean.Data.AC.ContextInformation α] → α → List ℕ → List ℕ - List.tail Batteries.Data.List.Basic
{α : Type u_1} → List α → List α - List.removeNth Batteries.Data.List.Basic
{α : Type u} → List α → ℕ → List α - List.removeNthTR Batteries.Data.List.Basic
{α : Type u_1} → List α → ℕ → List α - List.rotate Batteries.Data.List.Basic
{α : Type u_1} → List α → ℕ → List α - List.rotate' Batteries.Data.List.Basic
{α : Type u_1} → List α → ℕ → List α - List.after Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List α - List.dropSlice Batteries.Data.List.Basic
{α : Type u_1} → ℕ → ℕ → List α → List α - List.dropSliceTR Batteries.Data.List.Basic
{α : Type u_1} → ℕ → ℕ → List α → List α - List.eraseDup Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α - List.eraseP Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List α - List.erasePTR Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List α - List.insertNth Batteries.Data.List.Basic
{α : Type u_1} → ℕ → α → List α → List α - List.insertNthTR Batteries.Data.List.Basic
{α : Type u_1} → ℕ → α → List α → List α - List.leftpad Batteries.Data.List.Basic
{α : Type u_1} → ℕ → α → List α → List α - List.leftpadTR Batteries.Data.List.Basic
{α : Type u_1} → ℕ → α → List α → List α - List.modifyHead Batteries.Data.List.Basic
{α : Type u_1} → (α → α) → List α → List α - List.modifyLast Batteries.Data.List.Basic
{α : Type u_1} → (α → α) → List α → List α - List.sections Batteries.Data.List.Basic
{α : Type u_1} → List (List α) → List (List α) - List.sectionsTR Batteries.Data.List.Basic
{α : Type u_1} → List (List α) → List (List α) - List.takeD Batteries.Data.List.Basic
{α : Type u_1} → ℕ → List α → α → List α - List.takeDTR Batteries.Data.List.Basic
{α : Type u_1} → ℕ → List α → α → List α - List.transpose Batteries.Data.List.Basic
{α : Type u_1} → 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} → List (Option α) → List α → List α - List.lookmap Batteries.Data.List.Basic
{α : Type u_1} → (α → Option α) → List α → List α - List.modifyNth Batteries.Data.List.Basic
{α : Type u_1} → (α → α) → ℕ → List α → List α - List.modifyNthTR Batteries.Data.List.Basic
{α : Type u_1} → (α → α) → ℕ → List α → List α - List.replaceF Batteries.Data.List.Basic
{α : Type u_1} → (α → Option α) → List α → List α - List.replaceFTR Batteries.Data.List.Basic
{α : Type u_1} → (α → Option α) → List α → List α - List.bagInter Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α → List α - List.diff Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α → List α - List.inter Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α → List α - List.removeNth_eq_removeNthTR Batteries.Data.List.Basic
@List.eraseIdx = @List.eraseIdxTR - List.union Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α → List α - List.insertNthTR.go Batteries.Data.List.Basic
{α : Type u_1} → α → ℕ → List α → Array α → List α - List.modifyLast.go Batteries.Data.List.Basic
{α : Type u_1} → (α → α) → List α → Array α → List α - List.takeDTR.go Batteries.Data.List.Basic
{α : Type u_1} → α → ℕ → List α → Array α → List α - List.dropSlice_eq_dropSliceTR Batteries.Data.List.Basic
@List.dropSlice = @List.dropSliceTR - List.eraseP_eq_erasePTR Batteries.Data.List.Basic
@List.eraseP = @List.erasePTR - List.insertNth_eq_insertNthTR Batteries.Data.List.Basic
@List.insertNth = @List.insertNthTR - List.leftpad_eq_leftpadTR Batteries.Data.List.Basic
@List.leftpad = @List.leftpadTR - List.merge Batteries.Data.List.Basic
{α : Type u_1} → (α → α → Bool) → List α → List α → List α - List.modifyNthTail Batteries.Data.List.Basic
{α : Type u_1} → (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.lookmap.go Batteries.Data.List.Basic
{α : Type u_1} → (α → Option α) → List α → Array α → List α - List.modifyNthTR.go Batteries.Data.List.Basic
{α : Type u_1} → (α → α) → List α → ℕ → Array α → List α - List.replaceFTR.go Batteries.Data.List.Basic
{α : Type u_1} → (α → Option α) → List α → Array α → List α - List.fillNones_eq_fillNonesTR Batteries.Data.List.Basic
@List.fillNones = @List.fillNonesTR - List.modifyNth_eq_modifyNthTR Batteries.Data.List.Basic
@List.modifyNth = @List.modifyNthTR - List.pwFilter Batteries.Data.List.Basic
{α : Type u_1} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α - List.replaceF_eq_replaceFTR Batteries.Data.List.Basic
@List.replaceF = @List.replaceFTR - List.dropSliceTR.go Batteries.Data.List.Basic
{α : Type u_1} → List α → ℕ → List α → ℕ → Array α → List α - List.erasePTR.go Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List α → Array α → List α - List.merge.loop Batteries.Data.List.Basic
{α : Type u_1} → (α → α → Bool) → List α → List α → List α → List α - List.ofFnTR.go Batteries.Data.List.Basic
{α : Type u_1} → {n : ℕ} → (Fin n → α) → (i : ℕ) → i ≤ n → List α → List α - List.swapFirstTwo Mathlib.Tactic.ToAdditive
{α : Type u_1} → List α → List α - Batteries.DList.apply Batteries.Data.DList
{α : Type u} → Batteries.DList α → List α → List α - Batteries.RBNode.Path.withList Batteries.Data.RBMap.Lemmas
{α : Type u_1} → Batteries.RBNode.Path α → List α → List α - Mathlib.Tactic.MkIff.List.init Mathlib.Tactic.MkIffOfInductiveProp
{α : Type u_1} → List α → List α - List.dedup Mathlib.Data.List.Defs
{α : Type u_1} → [inst : DecidableEq α] → List α → List α - List.takeI Mathlib.Data.List.Defs
{α : Type u_1} → [inst : Inhabited α] → ℕ → List α → List α - List.replaceIf Mathlib.Data.List.Defs
{α : Type u_1} → List α → List Bool → List α → List α - List.destutter Mathlib.Data.List.Defs
{α : Type u_1} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α - List.destutter' Mathlib.Data.List.Defs
{α : Type u_1} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α - List.insertionSort Mathlib.Data.List.Sort
{α : Type uu} → (r : α → α → Prop) → [inst : DecidableRel r] → List α → List α - List.mergeSort Mathlib.Data.List.Sort
{α : Type uu} → (r : α → α → Prop) → [inst : DecidableRel r] → List α → List α - List.orderedInsert Mathlib.Data.List.Sort
{α : Type uu} → (r : α → α → Prop) → [inst : DecidableRel r] → α → List α → List α - List.sublistsAux Mathlib.Data.List.Sublists
{α : Type u} → α → List (List α) → List (List α) - List.sublists'Aux Mathlib.Data.List.Sublists
{α : Type u} → α → List (List α) → List (List α) → List (List α) - List.sublistsLenAux Mathlib.Data.List.Sublists
{α : Type u_1} → {β : Type u_2} → ℕ → List α → (List α → β) → List β → List β - FreeAddGroup.negRev Mathlib.GroupTheory.FreeGroup.Basic
{α : Type u} → List (α × Bool) → List (α × Bool) - FreeGroup.invRev Mathlib.GroupTheory.FreeGroup.Basic
{α : Type u} → List (α × Bool) → List (α × Bool) - FreeAddGroup.reduce Mathlib.GroupTheory.FreeGroup.Basic
{α : Type u} → [inst : DecidableEq α] → List (α × Bool) → List (α × Bool) - FreeGroup.reduce Mathlib.GroupTheory.FreeGroup.Basic
{α : Type u} → [inst : DecidableEq α] → List (α × Bool) → List (α × Bool) - Mathlib.MoveAdd.reorderUsing Mathlib.Tactic.MoveAdd
{α : Type u_1} → [inst : BEq α] → List α → List (α × Bool) → List α - Turing.TM2to1.stWrite Mathlib.Computability.TuringMachine
{K : Type u_1} → {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → σ → List (Γ k) → Turing.TM2to1.StAct k → List (Γ k) - List.dedupKeys Mathlib.Data.List.Sigma
{α : Type u} → {β : α → Type v} → [inst : DecidableEq α] → List (Sigma β) → List (Sigma β) - List.kerase Mathlib.Data.List.Sigma
{α : Type u} → {β : α → Type v} → [inst : DecidableEq α] → α → List (Sigma β) → List (Sigma β) - List.kinsert Mathlib.Data.List.Sigma
{α : Type u} → {β : α → Type v} → [inst : DecidableEq α] → (a : α) → β a → List (Sigma β) → List (Sigma β) - List.kreplace Mathlib.Data.List.Sigma
{α : Type u} → {β : α → Type v} → [inst : DecidableEq α] → (a : α) → β a → List (Sigma β) → List (Sigma β) - List.kunion Mathlib.Data.List.Sigma
{α : Type u} → {β : α → Type v} → [inst : DecidableEq α] → List (Sigma β) → List (Sigma β) → List (Sigma β) - List.rdrop Mathlib.Data.List.DropRight
{α : Type u_1} → List α → ℕ → List α - List.rtake Mathlib.Data.List.DropRight
{α : Type u_1} → List α → ℕ → List α - List.rdropWhile Mathlib.Data.List.DropRight
{α : Type u_1} → (α → Bool) → List α → List α - List.rtakeWhile Mathlib.Data.List.DropRight
{α : Type u_1} → (α → Bool) → List α → List α - LevenshteinEstimator'.pre_rev Mathlib.Data.List.EditDistance.Estimator
{α β δ : Type} → [inst : CanonicallyLinearOrderedAddCommMonoid δ] → {C : Levenshtein.Cost α β δ} → {xs : List α} → {ys : List β} → LevenshteinEstimator' C xs ys → List β - LevenshteinEstimator'.suff Mathlib.Data.List.EditDistance.Estimator
{α β δ : Type} → [inst : CanonicallyLinearOrderedAddCommMonoid δ] → {C : Levenshtein.Cost α β δ} → {xs : List α} → {ys : List β} → LevenshteinEstimator' C xs ys → List β
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the 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 findtsum_lt_tsum
even though the hypothesisf 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision 38aa2fc