Loogle!
Result
Found 8096 definitions mentioning List. Of these, 367 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.join Init.Data.List.Basic
{α : Type u} → List (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.enum Init.Data.List.Basic
{α : Type u} → 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.enumFrom 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.map Init.Data.List.Basic
{α : Type u} → {β : Type v} → (α → β) → List α → List β - List.mapTR Init.Data.List.Basic
{α : Type u} → {β : Type v} → (α → β) → List α → List β - List.bind Init.Data.List.Basic
{α : Type u} → {β : Type v} → List α → (α → List β) → List β - List.filterMap Init.Data.List.Basic
{α : Type u} → {β : Type v} → (α → Option β) → List α → List β - List.groupBy Init.Data.List.Basic
{α : Type u} → (α → α → Bool) → 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.zip Init.Data.List.Basic
{α : Type u} → {β : Type v} → List α → List β → List (α × β) - 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.map_eq_mapTR Init.Data.List.Basic
@List.map = @List.mapTR - List.zipWith Init.Data.List.Basic
{α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → List α → List β → List γ - List.zipWithAll Init.Data.List.Basic
{α : Type u} → {β : Type v} → {γ : Type w} → (Option α → Option β → γ) → 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.joinTR Init.Data.List.Impl
{α : Type u_1} → List (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.enumFromTR Init.Data.List.Impl
{α : Type u_1} → ℕ → List α → List (ℕ × α) - 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.bindTR Init.Data.List.Impl
{α : Type u_1} → {β : Type u_2} → List α → (α → List β) → List β - List.eraseIdx_eq_eraseIdxTR Init.Data.List.Impl
@List.eraseIdx = @List.eraseIdxTR - List.filterMapTR Init.Data.List.Impl
{α : Type u_1} → {β : Type u_2} → (α → Option β) → List α → List β - List.intersperse_eq_intersperseTR Init.Data.List.Impl
@List.intersperse = @List.intersperseTR - List.join_eq_joinTR Init.Data.List.Impl
@List.join = @List.joinTR - 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.enumFrom_eq_enumFromTR Init.Data.List.Impl
@List.enumFrom = @List.enumFromTR - 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.bindTR.go Init.Data.List.Impl
{α : Type u_1} → {β : Type u_2} → (α → List β) → List α → Array β → List β - List.filterMapTR.go Init.Data.List.Impl
{α : Type u_1} → {β : Type u_2} → (α → Option β) → List α → Array β → List β - 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.bind_eq_bindTR Init.Data.List.Impl
@List.bind = @List.bindTR - List.filterMap_eq_filterMapTR Init.Data.List.Impl
@List.filterMap = @List.filterMapTR - List.replace_eq_replaceTR Init.Data.List.Impl
@List.replace = @List.replaceTR - List.zipWithTR Init.Data.List.Impl
{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → List α → List β → List γ - 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 α - List.zipWithTR.go Init.Data.List.Impl
{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → List α → List β → Array γ → List γ - List.zipWith_eq_zipWithTR Init.Data.List.Impl
@List.zipWith = @List.zipWithTR - 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.ResolveName.resolveNamespaceUsingOpenDecls Lean.ResolveName
Lean.Environment → Lean.Name → List Lean.OpenDecl → List Lean.Name - Lean.ResolveName.resolveNamespace Lean.ResolveName
Lean.Environment → Lean.Name → List Lean.OpenDecl → Lean.Name → List Lean.Name - Lean.ResolveName.resolveGlobalName Lean.ResolveName
Lean.Environment → Lean.Name → List Lean.OpenDecl → Lean.Name → List (Lean.Name × List String) - Lean.ResolveName.resolveGlobalName.loop Lean.ResolveName
Lean.Environment → Lean.Name → List Lean.OpenDecl → Lean.MacroScopesView → Lean.Name → List String → List (Lean.Name × List String) - 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.Parser.resolveParserNameCore Lean.Parser.Extension
Lean.Environment → Lean.Name → List Lean.OpenDecl → Lean.Ident → List Lean.Parser.ParserName - 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.inits Batteries.Data.List.Basic
{α : Type u_1} → List α → List (List α) - List.initsTR Batteries.Data.List.Basic
{α : Type u_1} → List α → List (List α) - List.reduceOption Batteries.Data.List.Basic
{α : Type u_1} → List (Option α) → 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.sublists Batteries.Data.List.Basic
{α : Type u_1} → List α → List (List α) - List.sublists' Batteries.Data.List.Basic
{α : Type u_1} → List α → List (List α) - List.sublistsFast Batteries.Data.List.Basic
{α : Type u_1} → List α → List (List α) - List.tails Batteries.Data.List.Basic
{α : Type u_1} → List α → List (List α) - List.tailsTR Batteries.Data.List.Basic
{α : Type u_1} → List α → 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.findIdxs 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.revzip 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.toChunks Batteries.Data.List.Basic
{α : Type u_1} → ℕ → List α → 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.indexesOf Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → α → 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.splitOnP Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List (List α) - List.splitOnPTR Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → 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.indexesValues Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List (ℕ × α) - List.inits_eq_initsTR Batteries.Data.List.Basic
@List.inits = @List.initsTR - List.inter Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → List α → List α → List α - List.mapIdx Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → (ℕ → α → β) → List α → List β - List.removeNth_eq_removeNthTR Batteries.Data.List.Basic
@List.eraseIdx = @List.eraseIdxTR - List.splitOn Batteries.Data.List.Basic
{α : Type u_1} → [inst : BEq α] → α → List α → List (List α) - List.tails_eq_tailsTR Batteries.Data.List.Basic
@List.tails = @List.tailsTR - 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.tailsTR.go Batteries.Data.List.Basic
{α : Type u_1} → List α → Array (List α) → List (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.mapWithComplement Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → (α → List α → β) → List α → List β - 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.product Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → List α → List β → List (α × β) - List.productTR Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → List α → List β → List (α × β) - List.scanl Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → (α → β → α) → α → List β → List α - List.scanlTR Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → (α → β → α) → α → List β → List α - List.scanr Batteries.Data.List.Basic
{α : Type u_1} → {β : Type u_2} → (α → β → β) → β → 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.splitOnP.go Batteries.Data.List.Basic
{α : Type u_1} → (α → Bool) → List α → List α → List (List α) - List.fillNones_eq_fillNonesTR Batteries.Data.List.Basic
@List.fillNones = @List.fillNonesTR
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