Loogle!

Result

Found 2603 declarations mentioning String. Of these, 169 have a name containing "Name".

• Lean.Name.mkSimple 📋 Init.Prelude
  (s : String) : Lean.Name
• Lean.Name.mkStr1 📋 Init.Prelude
  (s₁ : String) : Lean.Name
• Lean.Name.mkStr 📋 Init.Prelude
  (p : Lean.Name) (s : String) : Lean.Name
• Lean.Name.mkStr2 📋 Init.Prelude
  (s₁ s₂ : String) : Lean.Name
• Lean.Name.str 📋 Init.Prelude
  (pre : Lean.Name) (str : String) : Lean.Name
• Lean.Name.mkStr3 📋 Init.Prelude
  (s₁ s₂ s₃ : String) : Lean.Name
• Lean.Name.mkStr4 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ : String) : Lean.Name
• Lean.Name.mkStr5 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ : String) : Lean.Name
• Lean.Macro.resolveGlobalName 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM (List (Lean.Name × List String))
• Lean.Name.mkStr6 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Lean.Name
• Lean.Name.mkStr7 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Lean.Name
• Lean.Macro.Methods.resolveGlobalName 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.Name → Lean.MacroM (List (Lean.Name × List String))
• Lean.Name.mkStr8 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Lean.Name
• Lean.Name.str.sizeOf_spec 📋 Init.SizeOf
  (p : Lean.Name) (s : String) : sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
• Lean.Name.str.injEq 📋 Init.Core
  (pre : Lean.Name) (str : String) (pre✝ : Lean.Name) (str✝ : String) : (pre.str str = pre✝.str str✝) = (pre = pre✝ ∧ str = str✝)
• String.toName 📋 Init.Meta
  (s : String) : Lean.Name
• Lean.Name.appendAfter 📋 Init.Meta
  (n : Lean.Name) (suffix : String) : Lean.Name
• Lean.Name.appendBefore 📋 Init.Meta
  (n : Lean.Name) (pre : String) : Lean.Name
• Lean.Syntax.decodeNameLit 📋 Init.Meta
  (s : String) : Option Lean.Name
• Lean.Name.toStringWithSep.maybeEscape 📋 Init.Meta
  (escape : Bool) (s : String) (force : Bool) : String
• Lean.Syntax.mkNameLit 📋 Init.Meta
  (val : String) (info : Lean.SourceInfo := Lean.SourceInfo.none) : Lean.NameLit
• Lean.Name.escapePart 📋 Init.Meta
  (s : String) (force : Bool := false) : Option String
• Lean.Name.toStringWithSep 📋 Init.Meta
  (sep : String) (escape : Bool) (n : Lean.Name) (isToken : String → Bool := fun x => false) : String
• Lean.Name.toString 📋 Init.Meta
  (n : Lean.Name) (escape : Bool := true) (isToken : String → Bool := fun x => false) : String
• System.FilePath.fileName 📋 Init.System.FilePath
  (p : System.FilePath) : Option String
• System.FilePath.withFileName 📋 Init.System.FilePath
  (p : System.FilePath) (fname : String) : System.FilePath
• IO.FS.DirEntry.fileName 📋 Init.System.IO
  (self : IO.FS.DirEntry) : String
• Std.Time.TimeZone.name 📋 Std.Time.Zoned.TimeZone
  (self : Std.Time.TimeZone) : String
• Std.Net.InterfaceAddress.name 📋 Std.Net.Addr
  (self : Std.Net.InterfaceAddress) : String
• Std.Internal.UV.System.osGetHostname 📋 Std.Internal.UV.System
  : IO String
• Std.Internal.UV.System.GroupInfo.groupname 📋 Std.Internal.UV.System
  (self : Std.Internal.UV.System.GroupInfo) : String
• Std.Internal.UV.System.PasswdInfo.username 📋 Std.Internal.UV.System
  (self : Std.Internal.UV.System.PasswdInfo) : String
• Std.Internal.UV.System.UnameInfo.machine 📋 Std.Internal.UV.System
  (self : Std.Internal.UV.System.UnameInfo) : String
• Std.Internal.UV.System.UnameInfo.release 📋 Std.Internal.UV.System
  (self : Std.Internal.UV.System.UnameInfo) : String
• Std.Internal.UV.System.UnameInfo.sysname 📋 Std.Internal.UV.System
  (self : Std.Internal.UV.System.UnameInfo) : String
• Std.Internal.UV.System.UnameInfo.version 📋 Std.Internal.UV.System
  (self : Std.Internal.UV.System.UnameInfo) : String
• Std.Internal.UV.System.UnameInfo.mk 📋 Std.Internal.UV.System
  (sysname release version machine : String) : Std.Internal.UV.System.UnameInfo
• Std.Internal.UV.System.UnameInfo.mk.injEq 📋 Std.Internal.UV.System
  (sysname release version machine sysname✝ release✝ version✝ machine✝ : String) : ({ sysname := sysname, release := release, version := version, machine := machine } = { sysname := sysname✝, release := release✝, version := version✝, machine := machine✝ }) = (sysname = sysname✝ ∧ release = release✝ ∧ version = version✝ ∧ machine = machine✝)
• Std.Internal.UV.System.UnameInfo.mk.sizeOf_spec 📋 Std.Internal.UV.System
  (sysname release version machine : String) : sizeOf { sysname := sysname, release := release, version := version, machine := machine } = 1 + sizeOf sysname + sizeOf release + sizeOf version + sizeOf machine
• Std.Internal.UV.DNS.getNameInfo 📋 Std.Internal.UV.DNS
  (host : Std.Net.SocketAddress) : IO (IO.Promise (Except IO.Error (String × String)))
• Std.Internal.IO.Async.DNS.NameInfo.host 📋 Std.Internal.Async.DNS
  (self : Std.Internal.IO.Async.DNS.NameInfo) : String
• Std.Internal.IO.Async.DNS.NameInfo.service 📋 Std.Internal.Async.DNS
  (self : Std.Internal.IO.Async.DNS.NameInfo) : String
• Std.Internal.IO.Async.DNS.NameInfo.mk 📋 Std.Internal.Async.DNS
  (host service : String) : Std.Internal.IO.Async.DNS.NameInfo
• Std.Internal.IO.Async.DNS.NameInfo.mk.injEq 📋 Std.Internal.Async.DNS
  (host service host✝ service✝ : String) : ({ host := host, service := service } = { host := host✝, service := service✝ }) = (host = host✝ ∧ service = service✝)
• Std.Internal.IO.Async.DNS.NameInfo.mk.sizeOf_spec 📋 Std.Internal.Async.DNS
  (host service : String) : sizeOf { host := host, service := service } = 1 + sizeOf host + sizeOf service
• Std.Internal.IO.Async.System.getHostName 📋 Std.Internal.Async.System
  : IO String
• Std.Internal.IO.Async.System.GroupInfo.groupName 📋 Std.Internal.Async.System
  (self : Std.Internal.IO.Async.System.GroupInfo) : String
• Std.Internal.IO.Async.System.OSInfo.name 📋 Std.Internal.Async.System
  (self : Std.Internal.IO.Async.System.OSInfo) : String
• Std.Internal.IO.Async.System.SystemUser.username 📋 Std.Internal.Async.System
  (self : Std.Internal.IO.Async.System.SystemUser) : String
• Lean.Name.getString! 📋 Lean.Data.Name
  : Lean.Name → String
• Lean.Name.eqStr 📋 Lean.Data.Name
  : Lean.Name → String → Bool
• Lean.Name.isInternalDetail.matchPrefix 📋 Lean.Data.Name
  (s pre : String) : Bool
• Lean.Name.anyS 📋 Lean.Data.Name
  (n : Lean.Name) (f : String → Bool) : Bool
• Lean.NamePart.str 📋 Lean.Data.NameTrie
  (s : String) : Lean.NamePart
• Lean.NamePart.str.injEq 📋 Lean.Data.NameTrie
  (s s✝ : String) : (Lean.NamePart.str s = Lean.NamePart.str s✝) = (s = s✝)
• Lean.NamePart.str.sizeOf_spec 📋 Lean.Data.NameTrie
  (s : String) : sizeOf (Lean.NamePart.str s) = 1 + sizeOf s
• Lean.Name.fromJson? 📋 Lean.Data.Json.FromToJson
  (j : Lean.Json) : Except String Lean.Name
• Lean.NameMap.fromJson? 📋 Lean.Data.Json.FromToJson
  {α : Type} [Lean.FromJson α] : Lean.Json → Except String (Lean.NameMap α)
• Lean.Expr.ctorName 📋 Lean.Expr
  : Lean.Expr → String
• Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcDecode 📋 Lean.Server.Rpc.Basic
  {α : Type} [TypeName α] (j : Lean.Json) : ExceptT String (ReaderT Lean.Server.RpcObjectStore Id) (Lean.Server.WithRpcRef α)
• Lean.errorNameSuffix 📋 Lean.Message
  : String
• Lean.BaseMessage.fileName 📋 Lean.Message
  {α : Type u} (self : Lean.BaseMessage α) : String
• Lean.ErrorExplanation.CodeInfo.parse.namedAttr 📋 Lean.ErrorExplanation
  : Std.Internal.Parsec.String.Parser (String × String)
• Lean.MonadLog.getFileName 📋 Lean.Log
  {m : Type → Type} [self : Lean.MonadLog m] : m String
• Lean.ResolveName.resolveGlobalName 📋 Lean.ResolveName
  (env : Lean.Environment) (ns : Lean.Name) (openDecls : List Lean.OpenDecl) (id : Lean.Name) : List (Lean.Name × List String)
• Lean.ensureReservedNameAvailable 📋 Lean.ResolveName
  {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (declName : Lean.Name) (suffix : String) : m Unit
• Lean.ResolveName.resolveGlobalName.loop 📋 Lean.ResolveName
  (env : Lean.Environment) (ns : Lean.Name) (openDecls : List Lean.OpenDecl) (extractionResult : Lean.MacroScopesView) (id : Lean.Name) (projs : List String) : List (Lean.Name × List String)
• Lean.resolveGlobalName 📋 Lean.ResolveName
  {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] (id : Lean.Name) : m (List (Lean.Name × List String))
• Lean.resolveLocalName 📋 Lean.ResolveName
  {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadLCtx m] (n : Lean.Name) : m (Option (Lean.Expr × List String))
• Lean.resolveLocalName.loop 📋 Lean.ResolveName
  {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] (view : Lean.MacroScopesView) (findLocalDecl? : Lean.MacroScopesView → Bool → Option Lean.LocalDecl) (n : Lean.Name) (projs : List String) (globalDeclFound : Bool) : m (Option (Lean.Expr × List String))
• Lean.Parser.InputContext.fileName 📋 Lean.Parser.Types
  (self : Lean.Parser.InputContext) : String
• Lean.Core.Context.fileName 📋 Lean.CoreM
  (self : Lean.Core.Context) : String
• Lean.Lsp.RenameFile.annotationId? 📋 Lean.Data.Lsp.Basic
  (self : Lean.Lsp.RenameFile) : Option String
• Lean.Lsp.RenameFile.mk 📋 Lean.Data.Lsp.Basic
  (oldUri newUri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options) (annotationId? : Option String) : Lean.Lsp.RenameFile
• Lean.Lsp.RenameFile.mk.injEq 📋 Lean.Data.Lsp.Basic
  (oldUri newUri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options) (annotationId? : Option String) (oldUri✝ newUri✝ : Lean.Lsp.DocumentUri) (options?✝ : Option Lean.Lsp.CreateFile.Options) (annotationId?✝ : Option String) : ({ oldUri := oldUri, newUri := newUri, options? := options?, annotationId? := annotationId? } = { oldUri := oldUri✝, newUri := newUri✝, options? := options?✝, annotationId? := annotationId?✝ }) = (oldUri = oldUri✝ ∧ newUri = newUri✝ ∧ options? = options?✝ ∧ annotationId? = annotationId?✝)
• Lean.Lsp.RenameFile.mk.sizeOf_spec 📋 Lean.Data.Lsp.Basic
  (oldUri newUri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options) (annotationId? : Option String) : sizeOf { oldUri := oldUri, newUri := newUri, options? := options?, annotationId? := annotationId? } = 1 + sizeOf oldUri + sizeOf newUri + sizeOf options? + sizeOf annotationId?
• Lean.realizeGlobalName 📋 Lean.ReservedNameAction
  (id : Lean.Name) : Lean.CoreM (List (Lean.Name × List String))
• Lean.Elab.realizeGlobalNameWithInfos 📋 Lean.Elab.InfoTree.Main
  (ref : Lean.Syntax) (id : Lean.Name) : Lean.CoreM (List (Lean.Name × List String))
• Lean.getExternNameFor 📋 Lean.Compiler.ExternAttr
  (env : Lean.Environment) (backend fn : Lean.Name) : Option String
• Lean.IR.getUnboxOpName 📋 Lean.Compiler.IR.Basic
  (t : Lean.IR.IRType) : String
• Lean.Elab.InlayHintLabel.name 📋 Lean.Elab.InfoTree.InlayHints
  (n : String) : Lean.Elab.InlayHintLabel
• Lean.Elab.InlayHintLabel.name.injEq 📋 Lean.Elab.InfoTree.InlayHints
  (n n✝ : String) : (Lean.Elab.InlayHintLabel.name n = Lean.Elab.InlayHintLabel.name n✝) = (n = n✝)
• Lean.Elab.InlayHintLabel.name.sizeOf_spec 📋 Lean.Elab.InfoTree.InlayHints
  (n : String) : sizeOf (Lean.Elab.InlayHintLabel.name n) = 1 + sizeOf n
• Lean.Elab.Term.LVal.fieldName 📋 Lean.Elab.Term
  (ref : Lean.Syntax) (name : String) (suffix? : Option Lean.Name) (fullRef : Lean.Syntax) : Lean.Elab.Term.LVal
• Lean.Elab.Term.MVarErrorInfo.logError.addArgName 📋 Lean.Elab.Term
  (mvarErrorInfo : Lean.Elab.Term.MVarErrorInfo) (msg : Lean.MessageData) (extra : String := "") : Lean.Elab.TermElabM Lean.MessageData
• Lean.Elab.Term.resolveName.process 📋 Lean.Elab.Term
  (stx : Lean.Syntax) (n : Lean.Name) (explicitLevels : List Lean.Level) (candidates : List (Lean.Name × List String)) : Lean.Elab.TermElabM (List (Lean.Expr × List String))
• Lean.Elab.Term.resolveName 📋 Lean.Elab.Term
  (stx : Lean.Syntax) (n : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) (explicitLevels : List Lean.Level) (expectedType? : Option Lean.Expr := none) : Lean.Elab.TermElabM (List (Lean.Expr × List String))
• Lean.Elab.Term.LVal.fieldName.injEq 📋 Lean.Elab.Term
  (ref : Lean.Syntax) (name : String) (suffix? : Option Lean.Name) (fullRef ref✝ : Lean.Syntax) (name✝ : String) (suffix?✝ : Option Lean.Name) (fullRef✝ : Lean.Syntax) : (Lean.Elab.Term.LVal.fieldName ref name suffix? fullRef = Lean.Elab.Term.LVal.fieldName ref✝ name✝ suffix?✝ fullRef✝) = (ref = ref✝ ∧ name = name✝ ∧ suffix? = suffix?✝ ∧ fullRef = fullRef✝)
• Lean.Elab.Term.LVal.fieldName.sizeOf_spec 📋 Lean.Elab.Term
  (ref : Lean.Syntax) (name : String) (suffix? : Option Lean.Name) (fullRef : Lean.Syntax) : sizeOf (Lean.Elab.Term.LVal.fieldName ref name suffix? fullRef) = 1 + sizeOf ref + sizeOf name + sizeOf suffix? + sizeOf fullRef
• Lean.Meta.isHCongrReservedNameSuffix 📋 Lean.Meta.CongrTheorems
  (s : String) : Bool
• Lean.Meta.isEqnReservedNameSuffix 📋 Lean.Meta.Eqns
  (s : String) : Bool
• Lean.Meta.mkEqLikeNameFor 📋 Lean.Meta.Eqns
  (env : Lean.Environment) (declName : Lean.Name) (suffix : String) : Lean.Name
• Lean.Meta.declFromEqLikeName 📋 Lean.Meta.Eqns
  (env : Lean.Environment) (name : Lean.Name) : Option (Lean.Name × String)
• Lean.Elab.Command.Context.fileName 📋 Lean.Elab.Command
  (self : Lean.Elab.Command.Context) : String
• Lean.Lsp.LeanModule.name 📋 Lean.Data.Lsp.Extra
  (self : Lean.Lsp.LeanModule) : String
• Lean.Lsp.CallHierarchyItem.name 📋 Lean.Data.Lsp.LanguageFeatures
  (self : Lean.Lsp.CallHierarchyItem) : String
• Lean.Lsp.InlayHintLabel.name 📋 Lean.Data.Lsp.LanguageFeatures
  (n : String) : Lean.Lsp.InlayHintLabel
• Lean.Lsp.ParameterInformationLabel.name 📋 Lean.Data.Lsp.LanguageFeatures
  (name : String) : Lean.Lsp.ParameterInformationLabel
• Lean.Lsp.RenameParams.newName 📋 Lean.Data.Lsp.LanguageFeatures
  (self : Lean.Lsp.RenameParams) : String
• Lean.Lsp.SemanticTokenModifier.names 📋 Lean.Data.Lsp.LanguageFeatures
  : Array String
• Lean.Lsp.SemanticTokenType.names 📋 Lean.Data.Lsp.LanguageFeatures
  : Array String
• Lean.Lsp.SymbolInformation.name 📋 Lean.Data.Lsp.LanguageFeatures
  (self : Lean.Lsp.SymbolInformation) : String
• Lean.Lsp.RenameParams.mk 📋 Lean.Data.Lsp.LanguageFeatures
  (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (newName : String) : Lean.Lsp.RenameParams
• Lean.Lsp.SymbolInformation.containerName? 📋 Lean.Data.Lsp.LanguageFeatures
  (self : Lean.Lsp.SymbolInformation) : Option String
• Lean.Lsp.DocumentSymbolAux.name 📋 Lean.Data.Lsp.LanguageFeatures
  {Self : Type} (self : Lean.Lsp.DocumentSymbolAux Self) : String
• Lean.Lsp.InlayHintLabel.name.injEq 📋 Lean.Data.Lsp.LanguageFeatures
  (n n✝ : String) : (Lean.Lsp.InlayHintLabel.name n = Lean.Lsp.InlayHintLabel.name n✝) = (n = n✝)
• Lean.Lsp.ParameterInformationLabel.name.injEq 📋 Lean.Data.Lsp.LanguageFeatures
  (name name✝ : String) : (Lean.Lsp.ParameterInformationLabel.name name = Lean.Lsp.ParameterInformationLabel.name name✝) = (name = name✝)
• Lean.Lsp.RenameParams.mk.injEq 📋 Lean.Data.Lsp.LanguageFeatures
  (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (newName : String) (toTextDocumentPositionParams✝ : Lean.Lsp.TextDocumentPositionParams) (newName✝ : String) : ({ toTextDocumentPositionParams := toTextDocumentPositionParams, newName := newName } = { toTextDocumentPositionParams := toTextDocumentPositionParams✝, newName := newName✝ }) = (toTextDocumentPositionParams = toTextDocumentPositionParams✝ ∧ newName = newName✝)
• Lean.Lsp.InlayHintLabel.name.sizeOf_spec 📋 Lean.Data.Lsp.LanguageFeatures
  (n : String) : sizeOf (Lean.Lsp.InlayHintLabel.name n) = 1 + sizeOf n
• Lean.Lsp.ParameterInformationLabel.name.sizeOf_spec 📋 Lean.Data.Lsp.LanguageFeatures
  (name : String) : sizeOf (Lean.Lsp.ParameterInformationLabel.name name) = 1 + sizeOf name
• Lean.Lsp.RenameParams.mk.sizeOf_spec 📋 Lean.Data.Lsp.LanguageFeatures
  (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (newName : String) : sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams, newName := newName } = 1 + sizeOf toTextDocumentPositionParams + sizeOf newName
• Lean.Lsp.WorkspaceFolder.name 📋 Lean.Data.Lsp.Workspace
  (self : Lean.Lsp.WorkspaceFolder) : String
• Lean.Lsp.ClientInfo.name 📋 Lean.Data.Lsp.InitShutdown
  (self : Lean.Lsp.ClientInfo) : String
• Lean.Lsp.ServerInfo.name 📋 Lean.Data.Lsp.InitShutdown
  (self : Lean.Lsp.ServerInfo) : String
• Lean.Lsp.RefInfo.ParentDecl.name 📋 Lean.Data.Lsp.Internal
  (self : Lean.Lsp.RefInfo.ParentDecl) : String
• Lean.Widget.InteractiveGoal.userName? 📋 Lean.Widget.InteractiveGoal
  (self : Lean.Widget.InteractiveGoal) : Option String
• Lean.Widget.InteractiveHypothesisBundle.names 📋 Lean.Widget.InteractiveGoal
  (self : Lean.Widget.InteractiveHypothesisBundle) : Array String
• Lean.Elab.Tactic.Doc.TacticDoc.userName 📋 Lean.Elab.Tactic.Doc
  (self : Lean.Elab.Tactic.Doc.TacticDoc) : String
• Lean.Linter.MissingDocs.lintNamed 📋 Lean.Linter.MissingDocs
  (stx : Lean.Syntax) (msg : String) : Lean.Elab.Command.CommandElabM Unit
• Lean.NameMapAttributeImpl.descr 📋 Batteries.Lean.NameMapAttribute
  {α : Type} (self : Lean.NameMapAttributeImpl α) : String
• Lean.NameMapAttributeImpl.mk 📋 Batteries.Lean.NameMapAttribute
  {α : Type} (name : Lean.Name) (ref : Lean.Name := by exact decl_name%) (descr : String) (add : Lean.Name → Lean.Syntax → Lean.AttrM α) : Lean.NameMapAttributeImpl α
• Lean.NameMapAttributeImpl.mk.injEq 📋 Batteries.Lean.NameMapAttribute
  {α : Type} (name : Lean.Name) (ref : Lean.Name := by exact decl_name%) (descr : String) (add : Lean.Name → Lean.Syntax → Lean.AttrM α) (name✝ : Lean.Name) (ref✝ : Lean.Name := by exact decl_name%) (descr✝ : String) (add✝ : Lean.Name → Lean.Syntax → Lean.AttrM α) : ({ name := name, ref := ref, descr := descr, add := add } = { name := name✝, ref := ref✝, descr := descr✝, add := add✝ }) = (name = name✝ ∧ ref = ref✝ ∧ descr = descr✝ ∧ add = add✝)
• Lean.NameMapAttributeImpl.mk.sizeOf_spec 📋 Batteries.Lean.NameMapAttribute
  {α : Type} [SizeOf α] (name : Lean.Name) (ref : Lean.Name := by exact decl_name%) (descr : String) (add : Lean.Name → Lean.Syntax → Lean.AttrM α) : sizeOf { name := name, ref := ref, descr := descr, add := add } = 1 + sizeOf name + sizeOf ref + sizeOf descr
• Lean.Elab.Command.mkNameFromParserSyntax.appendCatName 📋 Lean.Elab.Syntax
  (catName : Lean.Name) (str : String) : String
• Lean.Elab.Command.mkNameFromParserSyntax.visit 📋 Lean.Elab.Syntax
  (stx : Lean.Syntax) (acc : String) : String
• Lean.Widget.UserWidgetDefinition.name 📋 Lean.Widget.UserWidget
  (self : Lean.Widget.UserWidgetDefinition) : String
• Lean.Widget.PanelWidgetInstance.name? 📋 Lean.Widget.UserWidget
  (self : Lean.Widget.PanelWidgetInstance) : Option String
• Lean.Elab.Command.NameGen.mkBaseName 📋 Lean.Elab.DeclNameGen
  (e : Lean.Expr) : Lean.Elab.Command.NameGen.MkNameM✝ String
• Lean.Elab.Command.NameGen.mkBaseNameWithSuffix 📋 Lean.Elab.DeclNameGen
  (pre : String) (type : Lean.Expr) : Lean.MetaM Lean.Name
• Lean.Elab.Command.NameGen.mkBaseNameWithSuffix' 📋 Lean.Elab.DeclNameGen
  (pre : String) (binders : Array Lean.Syntax) (type : Lean.Syntax) : Lean.Elab.TermElabM Lean.Name
• Lean.Name.lastComponentAsString 📋 Mathlib.Lean.Expr.Basic
  : Lean.Name → String
• Lean.Name.updateLast 📋 Mathlib.Lean.Expr.Basic
  (f : String → String) : Lean.Name → Lean.Name
• Simps.Config.nameStem 📋 Mathlib.Tactic.Simps.Basic
  (self : Simps.Config) : Option String
• ToAdditive.guessName 📋 Mathlib.Tactic.ToAdditive.Frontend
  : String → String
• ToAdditive.nameDict 📋 Mathlib.Tactic.ToAdditive.Frontend
  : String → List String
• ToAdditive.applyNameDict 📋 Mathlib.Tactic.ToAdditive.Frontend
  : List String → List String
• ToAdditive.endCapitalNames 📋 Mathlib.Tactic.ToAdditive.Frontend
  : Std.TreeMap String (List String) compare
• Lean.Xml.Parser.EncName 📋 Lean.Data.Xml.Parser
  : Std.Internal.Parsec.String.Parser String
• Lean.Xml.Parser.Name 📋 Lean.Data.Xml.Parser
  : Std.Internal.Parsec.String.Parser String
• Lean.mkModuleInitializationFunctionName 📋 Lean.Compiler.NameMangling
  (moduleName : Lean.Name) : String
• Lean.Name.mangle 📋 Lean.Compiler.NameMangling
  (n : Lean.Name) (pre : String := "l_") : String
• Lean.IR.EmitC.toCInitName 📋 Lean.Compiler.IR.EmitC
  (n : Lean.Name) : Lean.IR.EmitC.M String
• Lean.IR.EmitC.toCName 📋 Lean.Compiler.IR.EmitC
  (n : Lean.Name) : Lean.IR.EmitC.M String
• LLVM.Value.getName 📋 Lean.Compiler.IR.LLVMBindings
  {ctx : LLVM.Context} (value : LLVM.Value ctx) : BaseIO String
• LLVM.getNamedFunction 📋 Lean.Compiler.IR.LLVMBindings
  {ctx : LLVM.Context} (m : LLVM.Module ctx) (name : String) : BaseIO (Option (LLVM.Value ctx))
• LLVM.getNamedGlobal 📋 Lean.Compiler.IR.LLVMBindings
  {ctx : LLVM.Context} (m : LLVM.Module ctx) (name : String) : BaseIO (Option (LLVM.Value ctx))
• Lean.IR.EmitLLVM.toCInitName 📋 Lean.Compiler.IR.EmitLLVM
  {llvmctx : LLVM.Context} (n : Lean.Name) : Lean.IR.EmitLLVM.M llvmctx String
• Lean.IR.EmitLLVM.toCName 📋 Lean.Compiler.IR.EmitLLVM
  {llvmctx : LLVM.Context} (n : Lean.Name) : Lean.IR.EmitLLVM.M llvmctx String
• Lean.Meta.Match.isCongrEqnReservedNameSuffix 📋 Lean.Meta.Match.MatchEqs
  (s : String) : Bool
• Lean.Firefox.Thread.name 📋 Lean.Util.Profiler
  (self : Lean.Firefox.Thread) : String
• Lean.Elab.Tactic.Omega.formatErrorMessage.varNameOf 📋 Lean.Elab.Tactic.Omega.Frontend
  (i : ℕ) : String
• Lean.Elab.Tactic.Omega.formatErrorMessage.varNames 📋 Lean.Elab.Tactic.Omega.Frontend
  (mask : Array Bool) : Lean.MetaM (Array String)
• Lean.Server.Test.Runner.Client.Hyp.names 📋 Lean.Server.Test.Runner
  (self : Lean.Server.Test.Runner.Client.Hyp) : Array String
• Lean.Linter.List.allowedArrayNames 📋 Lean.Linter.List
  : List String
• Lean.Linter.List.allowedListNames 📋 Lean.Linter.List
  : List String
• Lean.Linter.List.allowedVectorNames 📋 Lean.Linter.List
  : List String
• Lean.Linter.List.stripBinderName 📋 Lean.Linter.List
  (s : String) : String
• Aesop.LocalRuleSet.trace.printSimpSetName 📋 Aesop.RuleSet
  : Lean.Name → String
• Aesop.StatsExtensionEntry.fileName 📋 Aesop.Stats.Extension
  (self : Aesop.StatsExtensionEntry) : String
• Plausible.NamedBinder 📋 Plausible.Testable
  (_n : String) (p : Prop) : Prop
• Plausible.NamedBinder.eq_1 📋 Plausible.Testable
  (_n : String) (p : Prop) : Plausible.NamedBinder _n p = p
• LeanSearchClient.SearchResult.name 📋 LeanSearchClient.Syntax
  (self : LeanSearchClient.SearchResult) : String
• LeanSearchClient.SearchServer.name 📋 LeanSearchClient.Syntax
  (self : LeanSearchClient.SearchServer) : String
• LeanSearchClient.LoogleMatch.name 📋 LeanSearchClient.LoogleSyntax
  (self : LeanSearchClient.LoogleMatch) : String
• String.renameMetaVar 📋 Mathlib.Tactic.Widget.SelectPanelUtils
  (s : String) : String
• Mathlib.Tactic.Polyrith.SageError.name 📋 Mathlib.Tactic.Polyrith
  (self : Mathlib.Tactic.Polyrith.SageError) : String
• ProofWidgets.ExprPresentationData.userName 📋 ProofWidgets.Presentation.Expr
  (self : ProofWidgets.ExprPresentationData) : String
• ProofWidgets.ExprPresenter.userName 📋 ProofWidgets.Presentation.Expr
  (self : ProofWidgets.ExprPresenter) : String
• Loogle.Find.Arguments.namePats 📋 Loogle.Find
  (self : Loogle.Find.Arguments) : Array String

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 ff04530 serving mathlib revision 5eb29c4