Loogle!

Result

Found 17066 declarations mentioning List. Of these, only the first 200 are shown.

• List 📋 Init.Prelude
  (α : Type u) : Type u
• List.nil 📋 Init.Prelude
  {α : Type u} : List α
• List.toByteArray 📋 Init.Prelude
  (bs : List UInt8) : ByteArray
• List.utf8Encode 📋 Init.Prelude
  (l : List Char) : ByteArray
• String.utf8EncodeChar 📋 Init.Prelude
  (c : Char) : List UInt8
• Lean.MacroScopesView.scopes 📋 Init.Prelude
  (self : Lean.MacroScopesView) : List Lean.MacroScope
• instInhabitedList 📋 Init.Prelude
  {α : Type u_1} : Inhabited (List α)
• List.length 📋 Init.Prelude
  {α : Type u_1} : List α → ℕ
• List.lengthTR 📋 Init.Prelude
  {α : Type u_1} (as : List α) : ℕ
• Lean.Macro.resolveNamespace 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM (List Lean.Name)
• List.toByteArray.loop 📋 Init.Prelude
  : List UInt8 → ByteArray → ByteArray
• Lean.Syntax.Preresolved.decl 📋 Init.Prelude
  (n : Lean.Name) (fields : List String) : Lean.Syntax.Preresolved
• Array.mk 📋 Init.Prelude
  {α : Type u} (toList : List α) : Array α
• Array.toList 📋 Init.Prelude
  {α : Type u} (self : Array α) : List α
• List.lengthTRAux 📋 Init.Prelude
  {α : Type u_1} : List α → ℕ → ℕ
• List.toArray 📋 Init.Prelude
  {α : Type u_1} (xs : List α) : Array α
• Lean.Macro.Methods.resolveNamespace 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.Name → Lean.MacroM (List Lean.Name)
• Lean.Macro.State.traceMsgs 📋 Init.Prelude
  (self : Lean.Macro.State) : List (Lean.Name × String)
• instDecidableEqList 📋 Init.Prelude
  {α : Type u} [DecidableEq α] : DecidableEq (List α)
• List.concat 📋 Init.Prelude
  {α : Type u} : List α → α → List α
• List.cons 📋 Init.Prelude
  {α : Type u} (head : α) (tail : List α) : List α
• List.ctorElimType 📋 Init.Prelude
  {α : Type u} {motive : List α → Sort u_1} (ctorIdx : ℕ) : Sort (max 1 u_1 (imax (u + 1) (u + 1) u_1))
• List.flatten 📋 Init.Prelude
  {α : Type u_1} : List (List α) → List α
• Lean.MacroScopesView.mk 📋 Init.Prelude
  (name imported ctx : Lean.Name) (scopes : List Lean.MacroScope) : Lean.MacroScopesView
• Lean.Syntax.ident 📋 Init.Prelude
  (info : Lean.SourceInfo) (rawVal : Substring.Raw) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) : Lean.Syntax
• List.append 📋 Init.Prelude
  {α : Type u_1} (xs ys : List α) : List α
• List.set 📋 Init.Prelude
  {α : Type u_1} (l : List α) (n : ℕ) (a : α) : List α
• Lean.Macro.resolveGlobalName 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM (List (Lean.Name × List String))
• List.get 📋 Init.Prelude
  {α : Type u} (as : List α) : Fin as.length → α
• List.map 📋 Init.Prelude
  {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List β
• Lean.Macro.Methods.resolveGlobalName 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.Name → Lean.MacroM (List (Lean.Name × List String))
• List.flatMap 📋 Init.Prelude
  {α : Type u} {β : Type v} (b : α → List β) (as : List α) : List β
• List.foldl 📋 Init.Prelude
  {α : Type u} {β : Type v} (f : α → β → α) (init : α) : List β → α
• List.instDecidableEqNil 📋 Init.Prelude
  {α : Type u_1} (a : List α) : Decidable (a = [])
• List.instDecidableNilEq 📋 Init.Prelude
  {α : Type u_1} (a : List α) : Decidable ([] = a)
• ByteArray.IsValidUTF8.intro 📋 Init.Prelude
  {b : ByteArray} (m : List Char) (hm : b = m.utf8Encode) : b.IsValidUTF8
• List.hasDecEq 📋 Init.Prelude
  {α : Type u} [DecidableEq α] (a b : List α) : Decidable (a = b)
• List.brecOn.go 📋 Init.Prelude
  {α : Type u} {motive : List α → Sort u_1} (t : List α) (F_1 : (t : List α) → List.below t → motive t) : motive t ×' List.below t
• Lean.Macro.Methods.mk 📋 Init.Prelude
  (expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)) (getCurrNamespace : Lean.MacroM Lean.Name) (hasDecl : Lean.Name → Lean.MacroM Bool) (resolveNamespace : Lean.Name → Lean.MacroM (List Lean.Name)) (resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))) : Lean.Macro.Methods
• List.brecOn.eq 📋 Init.Prelude
  {α : Type u} {motive : List α → Sort u_1} (t : List α) (F_1 : (t : List α) → List.below t → motive t) : List.brecOn t F_1 = F_1 t (List.brecOn.go t F_1).2
• Lean.Syntax.brecOn.go 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u} (t : Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t) (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) : motive_1 t ×' t.below
• Lean.Syntax.brecOn_1.go 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u} (t : Array Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t) (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) : motive_2 t ×' Lean.Syntax.below_1 t
• Lean.Syntax.brecOn_2.go 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u} (t : List Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t) (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) : motive_3 t ×' Lean.Syntax.below_2 t
• Lean.Syntax.brecOn.eq 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u} (t : Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t) (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) : t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Syntax.brecOn.go t F_1 F_2 F_3).2
• Lean.Syntax.brecOn_1.eq 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u} (t : Array Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t) (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) : Lean.Syntax.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Syntax.brecOn_1.go t F_1 F_2 F_3).2
• Lean.Syntax.brecOn_2.eq 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u} (t : List Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t) (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) : Lean.Syntax.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Syntax.brecOn_2.go t F_1 F_2 F_3).2
• List.nil.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] : sizeOf [] = 1
• Array.mk.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] (toList : List α) : sizeOf { toList := toList } = 1 + sizeOf toList
• Lean.Macro.Methods.mk.sizeOf_spec 📋 Init.SizeOf
  (expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)) (getCurrNamespace : Lean.MacroM Lean.Name) (hasDecl : Lean.Name → Lean.MacroM Bool) (resolveNamespace : Lean.Name → Lean.MacroM (List Lean.Name)) (resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))) : sizeOf { expandMacro? := expandMacro?, getCurrNamespace := getCurrNamespace, hasDecl := hasDecl, resolveNamespace := resolveNamespace, resolveGlobalName := resolveGlobalName } = 1
• List.cons.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] (head : α) (tail : List α) : sizeOf (head :: tail) = 1 + sizeOf head + sizeOf tail
• Lean.MacroScopesView.mk.sizeOf_spec 📋 Init.SizeOf
  (name imported ctx : Lean.Name) (scopes : List Lean.MacroScope) : sizeOf { name := name, imported := imported, ctx := ctx, scopes := scopes } = 1 + sizeOf name + sizeOf imported + sizeOf ctx + sizeOf scopes
• Lean.Syntax.ident.sizeOf_spec 📋 Init.SizeOf
  (info : Lean.SourceInfo) (rawVal : Substring.Raw) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) : sizeOf (Lean.Syntax.ident info rawVal val preresolved) = 1 + sizeOf info + sizeOf rawVal + sizeOf val + sizeOf preresolved
• Array.mk.injEq 📋 Init.Core
  {α : Type u} (toList toList✝ : List α) : ({ toList := toList } = { toList := toList✝ }) = (toList = toList✝)
• List.cons.injEq 📋 Init.Core
  {α : Type u} (head : α) (tail : List α) (head✝ : α) (tail✝ : List α) : (head :: tail = head✝ :: tail✝) = (head = head✝ ∧ tail = tail✝)
• Lean.Syntax.ident.injEq 📋 Init.Core
  (info : Lean.SourceInfo) (rawVal : Substring.Raw) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) (info✝ : Lean.SourceInfo) (rawVal✝ : Substring.Raw) (val✝ : Lean.Name) (preresolved✝ : List Lean.Syntax.Preresolved) : (Lean.Syntax.ident info rawVal val preresolved = Lean.Syntax.ident info✝ rawVal✝ val✝ preresolved✝) = (info = info✝ ∧ rawVal = rawVal✝ ∧ val = val✝ ∧ preresolved = preresolved✝)
• Lean.Meta.Occurrences.neg 📋 Init.MetaTypes
  (idxs : List ℕ) : Lean.Meta.Occurrences
• Lean.Meta.Occurrences.pos 📋 Init.MetaTypes
  (idxs : List ℕ) : Lean.Meta.Occurrences
• Lean.Meta.instCoeListNatOccurrences 📋 Init.MetaTypes
  : Coe (List ℕ) Lean.Meta.Occurrences
• Lean.Meta.Occurrences.neg.injEq 📋 Init.MetaTypes
  (idxs idxs✝ : List ℕ) : (Lean.Meta.Occurrences.neg idxs = Lean.Meta.Occurrences.neg idxs✝) = (idxs = idxs✝)
• Lean.Meta.Occurrences.pos.injEq 📋 Init.MetaTypes
  (idxs idxs✝ : List ℕ) : (Lean.Meta.Occurrences.pos idxs = Lean.Meta.Occurrences.pos idxs✝) = (idxs = idxs✝)
• Lean.Meta.Occurrences.neg.sizeOf_spec 📋 Init.MetaTypes
  (idxs : List ℕ) : sizeOf (Lean.Meta.Occurrences.neg idxs) = 1 + sizeOf idxs
• Lean.Meta.Occurrences.pos.sizeOf_spec 📋 Init.MetaTypes
  (idxs : List ℕ) : sizeOf (Lean.Meta.Occurrences.pos idxs) = 1 + sizeOf idxs
• List.and 📋 Init.Data.List.Basic
  (bs : List Bool) : Bool
• List.or 📋 Init.Data.List.Basic
  (bs : List Bool) : Bool
• List.range 📋 Init.Data.List.Basic
  (n : ℕ) : List ℕ
• List.Nodup 📋 Init.Data.List.Basic
  {α : Type u} : List α → Prop
• List.instAppend 📋 Init.Data.List.Basic
  {α : Type u} : Append (List α)
• List.instEmptyCollection 📋 Init.Data.List.Basic
  {α : Type u} : EmptyCollection (List α)
• List.instHasSubset 📋 Init.Data.List.Basic
  {α : Type u} : HasSubset (List α)
• List.isEmpty 📋 Init.Data.List.Basic
  {α : Type u} : List α → Bool
• List.singleton 📋 Init.Data.List.Basic
  {α : Type u} (a : α) : List α
• List.Mem 📋 Init.Data.List.Basic
  {α : Type u} (a : α) : List α → Prop
• List.dropLast 📋 Init.Data.List.Basic
  {α : Type u_1} : List α → List α
• List.getLast? 📋 Init.Data.List.Basic
  {α : Type u} : List α → Option α
• List.getLastD 📋 Init.Data.List.Basic
  {α : Type u} (as : List α) (fallback : α) : α
• List.head? 📋 Init.Data.List.Basic
  {α : Type u} : List α → Option α
• List.headD 📋 Init.Data.List.Basic
  {α : Type u} (as : List α) (fallback : α) : α
• List.instMembership 📋 Init.Data.List.Basic
  {α : Type u} : Membership α (List α)
• List.replicate 📋 Init.Data.List.Basic
  {α : Type u} (n : ℕ) (a : α) : List α
• List.replicateTR 📋 Init.Data.List.Basic
  {α : Type u} (n : ℕ) (a : α) : List α
• List.reverse 📋 Init.Data.List.Basic
  {α : Type u} (as : List α) : List α
• List.tail 📋 Init.Data.List.Basic
  {α : Type u} : List α → List α
• List.range.loop 📋 Init.Data.List.Basic
  : ℕ → List ℕ → List ℕ
• List.IsInfix 📋 Init.Data.List.Basic
  {α : Type u} (l₁ l₂ : List α) : Prop
• List.IsPrefix 📋 Init.Data.List.Basic
  {α : Type u} (l₁ l₂ : List α) : Prop
• List.IsSuffix 📋 Init.Data.List.Basic
  {α : Type u} (l₁ l₂ : List α) : Prop
• List.Perm 📋 Init.Data.List.Basic
  {α : Type u} : List α → List α → Prop
• List.Sublist 📋 Init.Data.List.Basic
  {α : Type u_1} : List α → List α → Prop
• List.Subset 📋 Init.Data.List.Basic
  {α : Type u} (l₁ l₂ : List α) : Prop
• List.all 📋 Init.Data.List.Basic
  {α : Type u} : List α → (α → Bool) → Bool
• List.any 📋 Init.Data.List.Basic
  {α : Type u} (l : List α) (p : α → Bool) : Bool
• List.countP 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : ℕ
• List.drop 📋 Init.Data.List.Basic
  {α : Type u} (n : ℕ) (xs : List α) : List α
• List.eraseIdx 📋 Init.Data.List.Basic
  {α : Type u} (l : List α) (i : ℕ) : List α
• List.findIdx 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : ℕ
• List.instBEq 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] : BEq (List α)
• List.instLE 📋 Init.Data.List.Basic
  {α : Type u} [LT α] : LE (List α)
• List.instLT 📋 Init.Data.List.Basic
  {α : Type u} [LT α] : LT (List α)
• List.intersperse 📋 Init.Data.List.Basic
  {α : Type u} (sep : α) (l : List α) : List α
• List.intersperseTR 📋 Init.Data.List.Basic
  {α : Type u} (sep : α) (l : List α) : List α
• List.reduceOption 📋 Init.Data.List.Basic
  {α : Type u_1} : List (Option α) → List α
• List.tail? 📋 Init.Data.List.Basic
  {α : Type u} : List α → Option (List α)
• List.take 📋 Init.Data.List.Basic
  {α : Type u} (n : ℕ) (xs : List α) : List α
• List.Pairwise 📋 Init.Data.List.Basic
  {α : Type u} (R : α → α → Prop) : List α → Prop
• List.appendTR 📋 Init.Data.List.Basic
  {α : Type u} (as bs : List α) : List α
• List.contains 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (as : List α) (a : α) : Bool
• List.count 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) : List α → ℕ
• List.dropWhile 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) : List α → List α
• List.elem 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) (l : List α) : Bool
• 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 α] (as : List α) : List α
• List.filter 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : List α
• List.filterTR 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (as : List α) : List α
• List.find? 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) : List α → Option α
• List.findIdx? 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : Option ℕ
• List.findRev? 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) : List α → Option α
• List.idxOf 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) : List α → ℕ
• List.insertIdx 📋 Init.Data.List.Basic
  {α : Type u} (xs : List α) (i : ℕ) (a : α) : 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.length_eq_lengthTR 📋 Init.Data.List.Basic
  : @List.length = @List.lengthTR
• List.max? 📋 Init.Data.List.Basic
  {α : Type u} [Max α] : List α → Option α
• List.min? 📋 Init.Data.List.Basic
  {α : Type u} [Min α] : List α → Option α
• 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} (l fallback : List α) : List α
• List.takeWhile 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (xs : List α) : List α
• List.countP.go 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) : List α → ℕ → ℕ
• List.findIdx.go 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) : List α → ℕ → ℕ
• List.range'TR.go 📋 Init.Data.List.Basic
  (step : ℕ) : ℕ → ℕ → List ℕ → List ℕ
• List.replicateTR.loop 📋 Init.Data.List.Basic
  {α : Type u} (a : α) : ℕ → List α → List α
• List.beq 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] : List α → List α → Bool
• List.erase 📋 Init.Data.List.Basic
  {α : Type u_1} [BEq α] : List α → α → List α
• List.eraseDupsBy 📋 Init.Data.List.Basic
  {α : Type u_1} (r : α → α → Bool) (as : List α) : List α
• List.eraseRepsBy 📋 Init.Data.List.Basic
  {α : Type u_1} (r : α → α → Bool) : List α → List α
• List.idxOf? 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) : List α → Option ℕ
• 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.isPerm 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] : List α → List α → Bool
• List.isPrefixOf 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] : List α → List α → Bool
• List.isSublist 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] : List α → List α → Bool
• List.isSuffixOf 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (l₁ l₂ : List α) : Bool
• List.le 📋 Init.Data.List.Basic
  {α : Type u} [LT α] (as bs : List α) : Prop
• List.lt 📋 Init.Data.List.Basic
  {α : Type u} [LT α] : List α → List α → Prop
• List.mapTR 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (as : List α) : List β
• List.modify 📋 Init.Data.List.Basic
  {α : Type u} (l : List α) (i : ℕ) (f : α → α) : List α
• List.replicate_eq_replicateTR 📋 Init.Data.List.Basic
  : @List.replicate = @List.replicateTR
• List.sum 📋 Init.Data.List.Basic
  {α : Type u_1} [Add α] [Zero α] : List α → α
• List.findIdx?.go 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) : List α → ℕ → Option ℕ
• List.Lex 📋 Init.Data.List.Basic
  {α : Type u} (r : α → α → Prop) (as bs : List α) : Prop
• List.filterMap 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → Option β) : List α → List β
• List.findSome? 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → Option β) : List α → Option β
• List.findSomeRev? 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → Option β) : List α → Option β
• List.foldr 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β → β) (init : β) (l : List α) : β
• List.intersperse_eq_intersperseTR 📋 Init.Data.List.Basic
  : @List.intersperse = @List.intersperseTR
• List.isEqv 📋 Init.Data.List.Basic
  {α : Type u} (as bs : List α) (eqv : α → α → Bool) : Bool
• List.nodupDecidable 📋 Init.Data.List.Basic
  {α : Type u} [DecidableEq α] (l : List α) : Decidable l.Nodup
• List.removeAll 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (xs ys : List α) : List α
• List.replace 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (l : List α) (a b : α) : List α
• List.splitAt 📋 Init.Data.List.Basic
  {α : Type u} (n : ℕ) (l : List α) : List α × List α
• List.splitBy 📋 Init.Data.List.Basic
  {α : Type u} (R : α → α → Bool) : 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.dropLast_nil 📋 Init.Data.List.Basic
  {α : Type u} : [].dropLast = []
• List.filter_eq_filterTR 📋 Init.Data.List.Basic
  : @List.filter = @List.filterTR
• List.findFinIdx? 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : Option (Fin l.length)
• List.getLast 📋 Init.Data.List.Basic
  {α : Type u} (as : List α) : as ≠ [] → α
• List.head 📋 Init.Data.List.Basic
  {α : Type u} (as : List α) : as ≠ [] → α
• List.isPrefixOf? 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (l₁ l₂ : List α) : Option (List α)
• List.isSuffixOf? 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (l₁ l₂ : List α) : Option (List α)
• List.leftpad_eq_leftpadTR 📋 Init.Data.List.Basic
  : @List.leftpad = @List.leftpadTR
• List.modifyTailIdx 📋 Init.Data.List.Basic
  {α : Type u} (l : List α) (i : ℕ) (f : List α → List α) : List α
• List.partition 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (as : List α) : List α × List α
• List.reverse_nil 📋 Init.Data.List.Basic
  {α : Type u} : [].reverse = []
• List.span 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (as : List α) : List α × List α
• List.tail_nil 📋 Init.Data.List.Basic
  {α : Type u} : [].tail = []
• List.zip 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} : List α → List β → List (α × β)
• List.dropLast.eq_1 📋 Init.Data.List.Basic
  {α : Type u_1} : [].dropLast = []
• List.eraseDupsBy.loop 📋 Init.Data.List.Basic
  {α : Type u_1} (r : α → α → Bool) : List α → List α → List α
• List.mapTR.loop 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) : List α → List β → List β
• List.modifyTailIdx.go 📋 Init.Data.List.Basic
  {α : Type u} (f : List α → List α) : ℕ → List α → List α
• List.empty_eq 📋 Init.Data.List.Basic
  {α : Type u} : ∅ = []
• List.finIdxOf? 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) (l : List α) : Option (Fin l.length)
• List.flatten_nil 📋 Init.Data.List.Basic
  {α : Type u} : [].flatten = []
• List.lookup 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} [BEq α] : α → List (α × β) → Option β
• List.map_eq_mapTR 📋 Init.Data.List.Basic
  : @List.map = @List.mapTR
• List.range' 📋 Init.Data.List.Basic
  (start len : ℕ) (step : ℕ := 1) : List ℕ
• List.range'TR 📋 Init.Data.List.Basic
  (s n : ℕ) (step : ℕ := 1) : List ℕ
• List.range_zero 📋 Init.Data.List.Basic
  : List.range 0 = []
• List.unzip 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (l : List (α × β)) : List α × List β
• List.unzipTR 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (l : List (α × β)) : List α × List β
• List.Mem.head 📋 Init.Data.List.Basic
  {α : Type u} {a : α} (as : List α) : List.Mem a (a :: as)
• List.eraseRepsBy.loop 📋 Init.Data.List.Basic
  {α : Type u_1} (r : α → α → Bool) : α → List α → List α → List α
• List.drop_nil 📋 Init.Data.List.Basic
  {α : Type u} {i : ℕ} : List.drop i [] = []
• List.eraseIdx_nil 📋 Init.Data.List.Basic
  {α : Type u} {i : ℕ} : [].eraseIdx i = []
• List.instLawfulBEq 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] [LawfulBEq α] : LawfulBEq (List α)
• List.instReflBEq 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] [ReflBEq α] : ReflBEq (List α)
• List.intersperse_nil 📋 Init.Data.List.Basic
  {α : Type u} {sep : α} : List.intersperse sep [] = []

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 6ff4759 serving mathlib revision 4aa3a51