Loogle!
Result
Found 8096 definitions mentioning List. Of these, 232 match your pattern(s). Of these, only the first 200 are shown.
- 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.iotaTR.go Init.Data.List.Basic
ℕ → List ℕ → List ℕ - List.range.loop Init.Data.List.Basic
ℕ → 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 α) - String.extract.go₂ Init.Data.String.Basic
List Char → String.Pos → String.Pos → List Char - String.utf8SetAux Init.Data.String.Basic
Char → List Char → String.Pos → String.Pos → List Char - String.extract.go₁ Init.Data.String.Basic
List Char → String.Pos → String.Pos → String.Pos → List Char - String.splitAux Init.Data.String.Basic
String → (Char → Bool) → String.Pos → String.Pos → List String → List String - String.splitOnAux Init.Data.String.Basic
String → String → String.Pos → String.Pos → String.Pos → List String → List String - Substring.splitOn.loop Init.Data.String.Basic
Substring → optParam String " " → String.Pos → String.Pos → String.Pos → List Substring → List Substring - Nat.toSubDigitsAux Init.Data.Repr
ℕ → List Char → List Char - Nat.toSuperDigitsAux Init.Data.Repr
ℕ → List Char → List Char - Nat.toDigitsCore Init.Data.Repr
ℕ → ℕ → ℕ → List Char → List Char - ReprTuple.mk Init.Data.Repr
{α : Type u} → (α → List Lean.Format → List Lean.Format) → ReprTuple α - 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 α - ByteArray.toList.loop Init.Data.ByteArray.Basic
ByteArray → ℕ → List UInt8 → List UInt8 - 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.mapA.eq_2 Init.Data.List.Lemmas
∀ {m : Type u → Type v} [inst : Applicative m] {α : Type w} {β : Type u} (f : α → m β) (a : α) (as : List α), List.mapA f (a :: as) = Seq.seq (List.cons <$> f a) fun x => List.mapA f as - Lean.Omega.Coeffs.toList Init.Omega.Coeffs
Lean.Omega.Coeffs → 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 α - FloatArray.toList.loop Init.Data.FloatArray.Basic
FloatArray → ℕ → List Float → List Float - Lean.Data.AC.mergeIdem Init.Data.AC
List ℕ → List ℕ - Lean.Data.AC.sort Init.Data.AC
List ℕ → List ℕ - Lean.Data.AC.insert Init.Data.AC
ℕ → List ℕ → List ℕ - Lean.Data.AC.mergeIdem.loop Init.Data.AC
ℕ → List ℕ → List ℕ - Lean.Data.AC.sort.loop Init.Data.AC
List ℕ → List ℕ → 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 ℕ - Lean.KVMap.insertCore Lean.Data.KVMap
List (Lean.Name × Lean.DataValue) → Lean.Name → Lean.DataValue → List (Lean.Name × Lean.DataValue) - Lean.Parser.ParserInfo.collectTokens Lean.Parser.Types
Lean.Parser.ParserInfo → List Lean.Parser.Token → List Lean.Parser.Token - Lean.Parser.ParserInfo.mk Lean.Parser.Types
(List Lean.Parser.Token → List Lean.Parser.Token) → (Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet) → Lean.Parser.FirstTokens → Lean.Parser.ParserInfo - Lean.Parser.ParserInfo.mk.sizeOf_spec Lean.Parser.Types
∀ (collectTokens : List Lean.Parser.Token → List Lean.Parser.Token) (collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet) (firstTokens : Lean.Parser.FirstTokens), sizeOf { collectTokens := collectTokens, collectKinds := collectKinds, firstTokens := firstTokens } = 1 + sizeOf firstTokens - Lean.Parser.ParserInfo.mk.injEq Lean.Parser.Types
∀ (collectTokens : List Lean.Parser.Token → List Lean.Parser.Token) (collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet) (firstTokens : Lean.Parser.FirstTokens) (collectTokens_1 : List Lean.Parser.Token → List Lean.Parser.Token) (collectKinds_1 : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet) (firstTokens_1 : Lean.Parser.FirstTokens), ({ collectTokens := collectTokens, collectKinds := collectKinds, firstTokens := firstTokens } = { collectTokens := collectTokens_1, collectKinds := collectKinds_1, firstTokens := firstTokens_1 }) = (collectTokens = collectTokens_1 ∧ collectKinds = collectKinds_1 ∧ firstTokens = firstTokens_1) - Lean.Elab.InfoTree.collectNodesBottomUp Lean.Server.InfoUtils
{α : Type} → (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List α → List α) → Lean.Elab.InfoTree → 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.range'TR.go Batteries.Data.List.Basic
optParam ℕ 1 → ℕ → ℕ → List ℕ → List ℕ - List.ofFnTR.go Batteries.Data.List.Basic
{α : Type u_1} → {n : ℕ} → (Fin n → α) → (i : ℕ) → i ≤ n → List α → List α - List.modifyNthTail.eq_2 Batteries.Data.List.Basic
∀ {α : Type u_1} (f : List α → List α) (n : ℕ), List.modifyNthTail f n.succ [] = [] - List.modifyNthTail.eq_1 Batteries.Data.List.Basic
∀ {α : Type u_1} (f : List α → List α) (x : List α), List.modifyNthTail f 0 x = f x - List.modifyNthTail.eq_3 Batteries.Data.List.Basic
∀ {α : Type u_1} (f : List α → List α) (n : ℕ) (a : α) (l : List α), List.modifyNthTail f n.succ (a :: l) = a :: List.modifyNthTail f n l - Lean.Meta.addSimpCongrTheoremEntry.insert Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem → List Lean.Meta.SimpCongrTheorem → List Lean.Meta.SimpCongrTheorem - Lean.Elab.Term.eraseNamedArg Lean.Elab.App
List Lean.Elab.Term.NamedArg → Lean.Name → List Lean.Elab.Term.NamedArg - Lean.Elab.Tactic.RCases.RCasesPatt.tuple₁Core Lean.Elab.Tactic.RCases
List Lean.Elab.Tactic.RCases.RCasesPatt → List Lean.Elab.Tactic.RCases.RCasesPatt - ToAdditive.applyNameDict Mathlib.Tactic.ToAdditive
List String → List String - ToAdditive.fixAbbreviation Mathlib.Tactic.ToAdditive
List String → List String - List.swapFirstTwo Mathlib.Tactic.ToAdditive
{α : Type u_1} → List α → List α - ToAdditive.capitalizeFirstLike Mathlib.Tactic.ToAdditive
String → List String → List String - String.splitCase Mathlib.Tactic.ToAdditive
String → optParam String.Pos 0 → optParam (List String) [] → List String - Lean.IR.UnreachableBranches.Value.addChoice Lean.Compiler.IR.ElimDeadBranches
(Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value) → List Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value → List Lean.IR.UnreachableBranches.Value - Lean.Compiler.LCNF.UnreachableBranches.Value.addChoice Lean.Compiler.LCNF.ElimDeadBranches
List Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Compiler.LCNF.UnreachableBranches.Value → List Lean.Compiler.LCNF.UnreachableBranches.Value - Lean.Elab.Tactic.GuardMsgs.MessageOrdering.apply Lean.Elab.GuardMsgs
Lean.Elab.Tactic.GuardMsgs.MessageOrdering → List String → List String - Lean.Elab.Term.MatchExpr.next Lean.Elab.MatchExpr
List Lean.Elab.Term.MatchExpr.Alt → Lean.Term → List Lean.Elab.Term.MatchExpr.Alt - List.filterMap_eq_filter Batteries.Data.List.Lemmas
∀ {α : Type u_1} (p : α → Bool), List.filterMap (Option.guard fun x => p x = true) = List.filter p - List.modifyNthTail_length Batteries.Data.List.Lemmas
∀ {α : Type u_1} (f : List α → List α), (∀ (l : List α), (f l).length = l.length) → ∀ (n : ℕ) (l : List α), (List.modifyNthTail f n l).length = l.length - List.modifyNthTail_eq_take_drop Batteries.Data.List.Lemmas
∀ {α : Type u_1} (f : List α → List α), f [] = [] → ∀ (n : ℕ) (l : List α), List.modifyNthTail f n l = List.take n l ++ f (List.drop n l) - List.modifyNthTail_add Batteries.Data.List.Lemmas
∀ {α : Type u_1} (f : List α → List α) (n : ℕ) (l₁ l₂ : List α), List.modifyNthTail f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂ - List.exists_of_modifyNthTail Batteries.Data.List.Lemmas
∀ {α : Type u_1} (f : List α → List α) {n : ℕ} {l : List α}, n ≤ l.length → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ List.modifyNthTail f n l = l₁ ++ f l₂ - Mathlib.Util.mkRecNames Mathlib.Util.CompileInductive
List Lean.Name → ℕ → List Lean.Name - Batteries.DList.apply Batteries.Data.DList
{α : Type u} → Batteries.DList α → List α → List α - Batteries.DList.mk Batteries.Data.DList
{α : Type u} → (apply : List α → List α) → (∀ (l : List α), apply l = apply [] ++ l) → Batteries.DList α - Batteries.DList.mk.sizeOf_spec Batteries.Data.DList
∀ {α : Type u} [inst : SizeOf α] (apply : List α → List α) (invariant : ∀ (l : List α), apply l = apply [] ++ l), sizeOf { apply := apply, invariant := invariant } = 1 - Batteries.DList.mk.injEq Batteries.Data.DList
∀ {α : Type u} (apply : List α → List α) (invariant : ∀ (l : List α), apply l = apply [] ++ l) (apply_1 : List α → List α) (invariant_1 : ∀ (l : List α), apply_1 l = apply_1 [] ++ l), ({ apply := apply, invariant := invariant } = { apply := apply_1, invariant := invariant_1 }) = (apply = apply_1) - 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 α - Mathlib.CountHeartbeats.variation Mathlib.Util.CountHeartbeats
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.length_modifyNthTail Mathlib.Data.List.Basic
∀ {α : Type u} (f : List α → List α), (∀ (l : List α), (f l).length = l.length) → ∀ (n : ℕ) (l : List α), (List.modifyNthTail f n l).length = l.length - List.modifyNthTail_modifyNthTail_same Mathlib.Data.List.Basic
∀ {α : Type u} {f g : List α → List α} (n : ℕ) (l : List α), List.modifyNthTail g n (List.modifyNthTail f n l) = List.modifyNthTail (g ∘ f) n l - List.modifyNthTail_modifyNthTail Mathlib.Data.List.Basic
∀ {α : Type u} {f g : List α → List α} (m n : ℕ) (l : List α), List.modifyNthTail g (m + n) (List.modifyNthTail f n l) = List.modifyNthTail (fun l => List.modifyNthTail g m (f l)) n l - List.modifyNthTail_modifyNthTail_le Mathlib.Data.List.Basic
∀ {α : Type u} {f g : List α → List α} (m n : ℕ) (l : List α), n ≤ m → List.modifyNthTail g m (List.modifyNthTail f n l) = List.modifyNthTail (fun l => List.modifyNthTail g (m - n) (f l)) n l - List.rel_append Mathlib.Data.List.Forall2
∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, (List.Forall₂ R ⇒ List.Forall₂ R ⇒ List.Forall₂ R) (fun x x_1 => x ++ x_1) fun x x_1 => x ++ x_1 - List.insertNth.eq_1 Mathlib.Data.List.InsertNth
∀ {α : Type u_1} (n : ℕ) (a : α), List.insertNth n a = List.modifyNthTail (List.cons a) n - 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 β - List.sublistsAux_eq_bind Mathlib.Data.List.Sublists
∀ {α : Type u}, List.sublistsAux = fun a r => r.bind fun l => [l, a :: l] - List.sublistsAux_eq_array_foldl Mathlib.Data.List.Sublists
∀ {α : Type u}, List.sublistsAux = fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] (List.toArray r) 0).toList - FreeAddMonoid.toList_comp_ofList Mathlib.Algebra.FreeMonoid.Basic
∀ {α : Type u_1}, ⇑FreeAddMonoid.toList ∘ ⇑FreeAddMonoid.ofList = id - FreeMonoid.toList_comp_ofList Mathlib.Algebra.FreeMonoid.Basic
∀ {α : Type u_1}, ⇑FreeMonoid.toList ∘ ⇑FreeMonoid.ofList = id
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