Loogle!

Result

Found 250 declarations mentioning String and Lean.Name. Of these, only the first 200 are shown.

• 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.Macro.trace 📋 Init.Prelude
  (clsName : Lean.Name) (msg : String) : Lean.MacroM Unit
• Lean.Name.mkStr3 📋 Init.Prelude
  (s₁ s₂ s₃ : String) : Lean.Name
• Lean.Syntax.Preresolved.decl 📋 Init.Prelude
  (n : Lean.Name) (fields : List String) : Lean.Syntax.Preresolved
• Lean.Name.mkStr4 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ : String) : Lean.Name
• Lean.Macro.State.traceMsgs 📋 Init.Prelude
  (self : Lean.Macro.State) : List (Lean.Name × String)
• Lean.Name.mkStr5 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ : String) : Lean.Name
• Lean.Macro.State.mk 📋 Init.Prelude
  (macroScope : Lean.MacroScope) (traceMsgs : List (Lean.Name × String)) : Lean.Macro.State
• 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.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
• 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
• Lean.Name.str.sizeOf_spec 📋 Init.SizeOf
  (p : Lean.Name) (s : String) : sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
• Lean.Macro.State.mk.sizeOf_spec 📋 Init.SizeOf
  (macroScope : Lean.MacroScope) (traceMsgs : List (Lean.Name × String)) : sizeOf { macroScope := macroScope, traceMsgs := traceMsgs } = 1 + sizeOf macroScope + sizeOf traceMsgs
• 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 📋 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
• Lean.KVMap.setString 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (v : String) : Lean.KVMap
• Lean.KVMap.updateString 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : String → String) : Lean.KVMap
• Lean.KVMap.getString 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : String := "") : String
• Lean.Name.getString! 📋 Lean.Data.Name
  : Lean.Name → String
• Lean.Name.eqStr 📋 Lean.Data.Name
  : Lean.Name → String → Bool
• Lean.Name.anyS 📋 Lean.Data.Name
  (n : Lean.Name) (f : String → Bool) : Bool
• Lean.getOptionDescr 📋 Lean.Data.Options
  (name : Lean.Name) : IO String
• Lean.OptionDecl.mk 📋 Lean.Data.Options
  (declName : Lean.Name := by exact decl_name%) (defValue : Lean.DataValue) (group descr : String) : Lean.OptionDecl
• Lean.OptionDecl.mk.injEq 📋 Lean.Data.Options
  (declName : Lean.Name := by exact decl_name%) (defValue : Lean.DataValue) (group descr : String) (declName✝ : Lean.Name := by exact decl_name%) (defValue✝ : Lean.DataValue) (group✝ descr✝ : String) : ({ declName := declName, defValue := defValue, group := group, descr := descr } = { declName := declName✝, defValue := defValue✝, group := group✝, descr := descr✝ }) = (declName = declName✝ ∧ defValue = defValue✝ ∧ group = group✝ ∧ descr = descr✝)
• Lean.OptionDecl.mk.sizeOf_spec 📋 Lean.Data.Options
  (declName : Lean.Name := by exact decl_name%) (defValue : Lean.DataValue) (group descr : String) : sizeOf { declName := declName, defValue := defValue, group := group, descr := descr } = 1 + sizeOf declName + sizeOf defValue + sizeOf group + sizeOf descr
• Std.Format.pretty' 📋 Lean.Data.Format
  (f : Std.Format) (o : Lean.Options := { }) : String
• Lean.Name.fromJson? 📋 Lean.Data.Json.FromToJson
  (j : Lean.Json) : Except String Lean.Name
• Lean.Json.parseTagged 📋 Lean.Data.Json.FromToJson
  (json : Lean.Json) (tag : String) (nFields : ℕ) (fieldNames? : Option (Array Lean.Name)) : Except String (Array Lean.Json)
• Lean.Syntax.mkAntiquotNode 📋 Lean.Syntax
  (kind : Lean.Name) (term : Lean.Syntax) (nesting : ℕ := 0) (name : Option String := none) (isPseudoKind : Bool := false) : Lean.Syntax
• Lean.modToFilePath 📋 Lean.Util.Path
  (base : System.FilePath) (mod : Lean.Name) (ext : String) : System.FilePath
• Lean.SearchPath.findModuleWithExt 📋 Lean.Util.Path
  (sp : Lean.SearchPath) (ext : String) (mod : Lean.Name) : IO (Option System.FilePath)
• Lean.SearchPath.findWithExt 📋 Lean.Util.Path
  (sp : Lean.SearchPath) (ext : String) (mod : Lean.Name) : IO (Option System.FilePath)
• Lean.profileit 📋 Lean.Util.Profile
  {α : Type} (category : String) (opts : Lean.Options) (fn : Unit → α) (decl : Lean.Name := Lean.Name.anonymous) : α
• Lean.profileitIO 📋 Lean.Util.Profile
  {ε α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) (decl : Lean.Name := Lean.Name.anonymous) : EIO ε α
• Lean.profileitIOUnsafe 📋 Lean.Util.Profile
  {ε α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) (decl : Lean.Name := Lean.Name.anonymous) : EIO ε α
• Lean.profileitM 📋 Lean.Util.Profile
  {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Lean.Options) (act : m α) (decl : Lean.Name := Lean.Name.anonymous) : m α
• Lean.Environment.evalConstCheck 📋 Lean.Environment
  (α : Type) (env : Lean.Environment) (opts : Lean.Options) (typeName constName : Lean.Name) : ExceptT String Id α
• Lean.Environment.evalConst 📋 Lean.Environment
  (α : Type u_1) (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) (checkMeta : Bool := true) : Except String α
• Lean.SerialMessage.mk 📋 Lean.Message
  (toBaseMessage : Lean.BaseMessage String) (kind : Lean.Name) : Lean.SerialMessage
• Lean.TraceData.mk 📋 Lean.Message
  (cls : Lean.Name) (startTime stopTime : Float) (collapsed : Bool) (tag : String) : Lean.TraceData
• Lean.mkErrorStringWithPos 📋 Lean.Message
  (fileName : String) (pos : Lean.Position) (msg : String) (endPos : Option Lean.Position := none) (kind : Option String := none) (name : Option Lean.Name := none) : String
• Lean.SerialMessage.mk.injEq 📋 Lean.Message
  (toBaseMessage : Lean.BaseMessage String) (kind : Lean.Name) (toBaseMessage✝ : Lean.BaseMessage String) (kind✝ : Lean.Name) : ({ toBaseMessage := toBaseMessage, kind := kind } = { toBaseMessage := toBaseMessage✝, kind := kind✝ }) = (toBaseMessage = toBaseMessage✝ ∧ kind = kind✝)
• Lean.SerialMessage.mk.sizeOf_spec 📋 Lean.Message
  (toBaseMessage : Lean.BaseMessage String) (kind : Lean.Name) : sizeOf { toBaseMessage := toBaseMessage, kind := kind } = 1 + sizeOf toBaseMessage + sizeOf kind
• Lean.TraceData.mk.injEq 📋 Lean.Message
  (cls : Lean.Name) (startTime stopTime : Float) (collapsed : Bool) (tag : String) (cls✝ : Lean.Name) (startTime✝ stopTime✝ : Float) (collapsed✝ : Bool) (tag✝ : String) : ({ cls := cls, startTime := startTime, stopTime := stopTime, collapsed := collapsed, tag := tag } = { cls := cls✝, startTime := startTime✝, stopTime := stopTime✝, collapsed := collapsed✝, tag := tag✝ }) = (cls = cls✝ ∧ startTime = startTime✝ ∧ stopTime = stopTime✝ ∧ collapsed = collapsed✝ ∧ tag = tag✝)
• Lean.TraceData.mk.sizeOf_spec 📋 Lean.Message
  (cls : Lean.Name) (startTime stopTime : Float) (collapsed : Bool) (tag : String) : sizeOf { cls := cls, startTime := startTime, stopTime := stopTime, collapsed := collapsed, tag := tag } = 1 + sizeOf cls + sizeOf startTime + sizeOf stopTime + sizeOf collapsed + sizeOf tag
• Lean.withTraceNode' 📋 Lean.Util.Trace
  {α : Type} {m : Type → Type} [Monad m] [Lean.MonadTrace m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept Lean.Exception m] [MonadLiftT BaseIO m] (cls : Lean.Name) (k : m (α × Lean.MessageData)) (collapsed : Bool := true) (tag : String := "") : m α
• Lean.withTraceNode 📋 Lean.Util.Trace
  {α : Type} {m : Type → Type} [Monad m] [Lean.MonadTrace m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] {ε : Type} [always : Lean.MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Lean.Name) (msg : Except ε α → m Lean.MessageData) (k : m α) (collapsed : Bool := true) (tag : String := "") : m α
• Lean.withTraceNodeBefore 📋 Lean.Util.Trace
  {α : Type} {m : Type → Type} [Monad m] [Lean.MonadTrace m] {ε : Type} [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [always : Lean.MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [Lean.ExceptToEmoji ε α] (cls : Lean.Name) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) (tag : String := "") : m α
• 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.filterFieldList 📋 Lean.ResolveName
  {m : Type → Type} [Monad m] [Lean.MonadError m] (n : Lean.Name) (cs : List (Lean.Name × List String)) : m (List Lean.Name)
• 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.isAuxRecursorWithSuffix 📋 Lean.AuxRecursor
  (env : Lean.Environment) (declName : Lean.Name) (suffix : String) : Bool
• Lean.Compiler.checkIsDefinition 📋 Lean.Compiler.Old
  (env : Lean.Environment) (n : Lean.Name) : Except String Unit
• Lean.addBuiltinDocString 📋 Lean.DocString.Extension
  (declName : Lean.Name) (docString : String) : IO Unit
• Lean.findSimpleDocString? 📋 Lean.DocString.Extension
  (env : Lean.Environment) (declName : Lean.Name) (includeBuiltin : Bool := true) : IO (Option String)
• Lean.addDocStringCore 📋 Lean.DocString.Extension
  {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadEnv m] (declName : Lean.Name) (docString : String) : m Unit
• Lean.addDocStringCore' 📋 Lean.DocString.Extension
  {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadEnv m] (declName : Lean.Name) (docString? : Option String) : m Unit
• Lean.Core.checkMaxHeartbeatsCore 📋 Lean.CoreM
  (moduleName : String) (optionName : Lean.Name) (max : ℕ) : Lean.CoreM Unit
• Lean.Core.Context.mk 📋 Lean.CoreM
  (fileName : String) (fileMap : Lean.FileMap) (options : Lean.Options) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (initHeartbeats maxHeartbeats : ℕ) (currMacroScope : Lean.MacroScope) (diag : Bool) (cancelTk? : Option IO.CancelToken) (suppressElabErrors : Bool) (inheritedTraceOptions : Std.HashSet Lean.Name) : Lean.Core.Context
• Lean.Core.Context.mk.injEq 📋 Lean.CoreM
  (fileName : String) (fileMap : Lean.FileMap) (options : Lean.Options) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (initHeartbeats maxHeartbeats : ℕ) (currMacroScope : Lean.MacroScope) (diag : Bool) (cancelTk? : Option IO.CancelToken) (suppressElabErrors : Bool) (inheritedTraceOptions : Std.HashSet Lean.Name) (fileName✝ : String) (fileMap✝ : Lean.FileMap) (options✝ : Lean.Options) (currRecDepth✝ maxRecDepth✝ : ℕ) (ref✝ : Lean.Syntax) (currNamespace✝ : Lean.Name) (openDecls✝ : List Lean.OpenDecl) (initHeartbeats✝ maxHeartbeats✝ : ℕ) (currMacroScope✝ : Lean.MacroScope) (diag✝ : Bool) (cancelTk?✝ : Option IO.CancelToken) (suppressElabErrors✝ : Bool) (inheritedTraceOptions✝ : Std.HashSet Lean.Name) : ({ fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls, initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, currMacroScope := currMacroScope, diag := diag, cancelTk? := cancelTk?, suppressElabErrors := suppressElabErrors, inheritedTraceOptions := inheritedTraceOptions } = { fileName := fileName✝, fileMap := fileMap✝, options := options✝, currRecDepth := currRecDepth✝, maxRecDepth := maxRecDepth✝, ref := ref✝, currNamespace := currNamespace✝, openDecls := openDecls✝, initHeartbeats := initHeartbeats✝, maxHeartbeats := maxHeartbeats✝, currMacroScope := currMacroScope✝, diag := diag✝, cancelTk? := cancelTk?✝, suppressElabErrors := suppressElabErrors✝, inheritedTraceOptions := inheritedTraceOptions✝ }) = (fileName = fileName✝ ∧ fileMap = fileMap✝ ∧ options = options✝ ∧ currRecDepth = currRecDepth✝ ∧ maxRecDepth = maxRecDepth✝ ∧ ref = ref✝ ∧ currNamespace = currNamespace✝ ∧ openDecls = openDecls✝ ∧ initHeartbeats = initHeartbeats✝ ∧ maxHeartbeats = maxHeartbeats✝ ∧ currMacroScope = currMacroScope✝ ∧ diag = diag✝ ∧ cancelTk? = cancelTk?✝ ∧ suppressElabErrors = suppressElabErrors✝ ∧ inheritedTraceOptions = inheritedTraceOptions✝)
• Lean.Core.Context.mk.sizeOf_spec 📋 Lean.CoreM
  (fileName : String) (fileMap : Lean.FileMap) (options : Lean.Options) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (initHeartbeats maxHeartbeats : ℕ) (currMacroScope : Lean.MacroScope) (diag : Bool) (cancelTk? : Option IO.CancelToken) (suppressElabErrors : Bool) (inheritedTraceOptions : Std.HashSet Lean.Name) : sizeOf { fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls, initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, currMacroScope := currMacroScope, diag := diag, cancelTk? := cancelTk?, suppressElabErrors := suppressElabErrors, inheritedTraceOptions := inheritedTraceOptions } = 1 + sizeOf fileName + sizeOf fileMap + sizeOf options + sizeOf currRecDepth + sizeOf maxRecDepth + sizeOf ref + sizeOf currNamespace + sizeOf openDecls + sizeOf initHeartbeats + sizeOf maxHeartbeats + sizeOf currMacroScope + sizeOf diag + sizeOf cancelTk? + sizeOf suppressElabErrors + sizeOf inheritedTraceOptions
• Lean.getAttributeImpl 📋 Lean.Attributes
  (env : Lean.Environment) (attrName : Lean.Name) : Except String Lean.AttributeImpl
• Lean.mkAttributeImplOfConstant 📋 Lean.Attributes
  (env : Lean.Environment) (opts : Lean.Options) (declName : Lean.Name) : Except String Lean.AttributeImpl
• Lean.mkAttributeImplOfConstantUnsafe 📋 Lean.Attributes
  (env : Lean.Environment) (opts : Lean.Options) (declName : Lean.Name) : Except String Lean.AttributeImpl
• Lean.AttributeImplCore.mk 📋 Lean.Attributes
  (ref : Lean.Name := by exact decl_name%) (name : Lean.Name) (descr : String) (applicationTime : Lean.AttributeApplicationTime) : Lean.AttributeImplCore
• Lean.EnumAttributes.setValue 📋 Lean.Attributes
  {α : Type} (attrs : Lean.EnumAttributes α) (env : Lean.Environment) (decl : Lean.Name) (val : α) : Except String Lean.Environment
• Lean.ParametricAttribute.setParam 📋 Lean.Attributes
  {α : Type} (attr : Lean.ParametricAttribute α) (env : Lean.Environment) (decl : Lean.Name) (param : α) : Except String Lean.Environment
• Lean.registerTagAttribute 📋 Lean.Attributes
  (name : Lean.Name) (descr : String) (validate : Lean.Name → Lean.AttrM Unit := fun x => pure ()) (ref : Lean.Name := by exact decl_name%) (applicationTime : Lean.AttributeApplicationTime := Lean.AttributeApplicationTime.afterTypeChecking) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.EnvExtension.AsyncMode.mainOnly) : IO Lean.TagAttribute
• Lean.registerEnumAttributes 📋 Lean.Attributes
  {α : Type} (attrDescrs : List (Lean.Name × String × α)) (validate : Lean.Name → α → Lean.AttrM Unit := fun x x => pure ()) (applicationTime : Lean.AttributeApplicationTime := Lean.AttributeApplicationTime.afterTypeChecking) (ref : Lean.Name := by exact decl_name%) : IO (Lean.EnumAttributes α)
• Lean.AttributeImplCore.mk.injEq 📋 Lean.Attributes
  (ref : Lean.Name := by exact decl_name%) (name : Lean.Name) (descr : String) (applicationTime : Lean.AttributeApplicationTime) (ref✝ : Lean.Name := by exact decl_name%) (name✝ : Lean.Name) (descr✝ : String) (applicationTime✝ : Lean.AttributeApplicationTime) : ({ ref := ref, name := name, descr := descr, applicationTime := applicationTime } = { ref := ref✝, name := name✝, descr := descr✝, applicationTime := applicationTime✝ }) = (ref = ref✝ ∧ name = name✝ ∧ descr = descr✝ ∧ applicationTime = applicationTime✝)
• Lean.AttributeImplCore.mk.sizeOf_spec 📋 Lean.Attributes
  (ref : Lean.Name := by exact decl_name%) (name : Lean.Name) (descr : String) (applicationTime : Lean.AttributeApplicationTime) : sizeOf { ref := ref, name := name, descr := descr, applicationTime := applicationTime } = 1 + sizeOf ref + sizeOf name + sizeOf descr + sizeOf applicationTime
• Lean.Compiler.setInlineAttribute 📋 Lean.Compiler.InlineAttrs
  (env : Lean.Environment) (declName : Lean.Name) (kind : Lean.Compiler.InlineAttributeKind) : Except String Lean.Environment
• 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.setBuiltinInitAttr 📋 Lean.Compiler.InitAttr
  (env : Lean.Environment) (declName : Lean.Name) (initFnName : Lean.Name := Lean.Name.anonymous) : Except String Lean.Environment
• Lean.ExternEntry.inline 📋 Lean.Compiler.ExternAttr
  (backend : Lean.Name) (pattern : String) : Lean.ExternEntry
• Lean.ExternEntry.standard 📋 Lean.Compiler.ExternAttr
  (backend : Lean.Name) (fn : String) : Lean.ExternEntry
• Lean.getExternNameFor 📋 Lean.Compiler.ExternAttr
  (env : Lean.Environment) (backend fn : Lean.Name) : Option String
• Lean.addExtern 📋 Lean.Compiler.ExternAttr
  (env : Lean.Environment) (n : Lean.Name) : ExceptT String Id Lean.Environment
• Lean.ExternEntry.inline.injEq 📋 Lean.Compiler.ExternAttr
  (backend : Lean.Name) (pattern : String) (backend✝ : Lean.Name) (pattern✝ : String) : (Lean.ExternEntry.inline backend pattern = Lean.ExternEntry.inline backend✝ pattern✝) = (backend = backend✝ ∧ pattern = pattern✝)
• Lean.ExternEntry.standard.injEq 📋 Lean.Compiler.ExternAttr
  (backend : Lean.Name) (fn : String) (backend✝ : Lean.Name) (fn✝ : String) : (Lean.ExternEntry.standard backend fn = Lean.ExternEntry.standard backend✝ fn✝) = (backend = backend✝ ∧ fn = fn✝)
• Lean.ExternEntry.inline.sizeOf_spec 📋 Lean.Compiler.ExternAttr
  (backend : Lean.Name) (pattern : String) : sizeOf (Lean.ExternEntry.inline backend pattern) = 1 + sizeOf backend + sizeOf pattern
• Lean.ExternEntry.standard.sizeOf_spec 📋 Lean.Compiler.ExternAttr
  (backend : Lean.Name) (fn : String) : sizeOf (Lean.ExternEntry.standard backend fn) = 1 + sizeOf backend + sizeOf fn
• Lean.KeyedDeclsAttribute.Def.mk 📋 Lean.KeyedDeclsAttribute
  {γ : Type} (builtinName name : Lean.Name) (descr : String) (valueTypeName : Lean.Name) (evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) (onAdded : Bool → Lean.Name → Lean.AttrM Unit) : Lean.KeyedDeclsAttribute.Def γ
• Lean.KeyedDeclsAttribute.Def.mk.sizeOf_spec 📋 Lean.KeyedDeclsAttribute
  {γ : Type} [SizeOf γ] (builtinName name : Lean.Name) (descr : String) (valueTypeName : Lean.Name) (evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) (onAdded : Bool → Lean.Name → Lean.AttrM Unit) : sizeOf { builtinName := builtinName, name := name, descr := descr, valueTypeName := valueTypeName, evalKey := evalKey, onAdded := onAdded } = 1 + sizeOf builtinName + sizeOf name + sizeOf descr + sizeOf valueTypeName
• Lean.KeyedDeclsAttribute.Def.mk.injEq 📋 Lean.KeyedDeclsAttribute
  {γ : Type} (builtinName name : Lean.Name) (descr : String) (valueTypeName : Lean.Name) (evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) (onAdded : Bool → Lean.Name → Lean.AttrM Unit) (builtinName✝ name✝ : Lean.Name) (descr✝ : String) (valueTypeName✝ : Lean.Name) (evalKey✝ : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) (onAdded✝ : Bool → Lean.Name → Lean.AttrM Unit) : ({ builtinName := builtinName, name := name, descr := descr, valueTypeName := valueTypeName, evalKey := evalKey, onAdded := onAdded } = { builtinName := builtinName✝, name := name✝, descr := descr✝, valueTypeName := valueTypeName✝, evalKey := evalKey✝, onAdded := onAdded✝ }) = (builtinName = builtinName✝ ∧ name = name✝ ∧ descr = descr✝ ∧ valueTypeName = valueTypeName✝ ∧ evalKey = evalKey✝ ∧ onAdded = onAdded✝)
• Lean.Parser.throwUnknownParserCategory 📋 Lean.Parser.Extension
  {α : Type} (catName : Lean.Name) : ExceptT String Id α
• Lean.Parser.addParserCategory 📋 Lean.Parser.Extension
  (env : Lean.Environment) (catName declName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior) : Except String Lean.Environment
• Lean.Parser.addLeadingParser 📋 Lean.Parser.Extension
  (categories : Lean.Parser.ParserCategories) (catName declName : Lean.Name) (p : Lean.Parser.Parser) (prio : ℕ) : Except String Lean.Parser.ParserCategories
• Lean.Parser.addTrailingParser 📋 Lean.Parser.Extension
  (categories : Lean.Parser.ParserCategories) (catName declName : Lean.Name) (p : Lean.Parser.TrailingParser) (prio : ℕ) : Except String Lean.Parser.ParserCategories
• Lean.Parser.addParser 📋 Lean.Parser.Extension
  (categories : Lean.Parser.ParserCategories) (catName declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : ℕ) : Except String Lean.Parser.ParserCategories
• Lean.Parser.runParserCategory 📋 Lean.Parser.Extension
  (env : Lean.Environment) (catName : Lean.Name) (input : String) (fileName : String := "<input>") : Except String Lean.Syntax
• Lean.ParserCompiler.registerCombinatorAttribute 📋 Lean.ParserCompiler.Attribute
  (name : Lean.Name) (descr : String) (ref : Lean.Name := by exact decl_name%) : IO Lean.ParserCompiler.CombinatorAttribute
• Lean.Parser.Term.Doc.getRecommendedSpellingString 📋 Lean.Parser.Term.Doc
  (env : Lean.Environment) (declName : Lean.Name) : String
• Lean.Meta.appendSection 📋 Lean.Meta.Diagnostics
  (m : Array Lean.MessageData) (cls : Lean.Name) (header : String) (s : Lean.Meta.DiagSummary) (resultSummary : Bool := true) : Array Lean.MessageData
• Lean.Linter.DeprecationEntry.mk 📋 Lean.Linter.Deprecated
  (newName? : Option Lean.Name) (text? since? : Option String) : Lean.Linter.DeprecationEntry
• Lean.Linter.DeprecationEntry.mk.injEq 📋 Lean.Linter.Deprecated
  (newName? : Option Lean.Name) (text? since? : Option String) (newName?✝ : Option Lean.Name) (text?✝ since?✝ : Option String) : ({ newName? := newName?, text? := text?, since? := since? } = { newName? := newName?✝, text? := text?✝, since? := since?✝ }) = (newName? = newName?✝ ∧ text? = text?✝ ∧ since? = since?✝)
• Lean.Linter.DeprecationEntry.mk.sizeOf_spec 📋 Lean.Linter.Deprecated
  (newName? : Option Lean.Name) (text? since? : Option String) : sizeOf { newName? := newName?, text? := text?, since? := since? } = 1 + sizeOf newName? + sizeOf text? + sizeOf since?
• Lean.Elab.evalSyntaxConstant 📋 Lean.Elab.Util
  (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) : ExceptT String Id Lean.Syntax
• Lean.Elab.mkElabAttribute 📋 Lean.Elab.Util
  (γ : Type) (attrBuiltinName attrName parserNamespace typeName : Lean.Name) (kind : String) (attrDeclName : Lean.Name := by exact decl_name%) : IO (Lean.KeyedDeclsAttribute γ)
• 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.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.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.Parser.Tactic.Doc.getTacticExtensionString 📋 Lean.Parser.Tactic.Doc
  (env : Lean.Environment) (tactic : Lean.Name) : String
• Lean.Parser.Tactic.Doc.getTacticExtensions 📋 Lean.Parser.Tactic.Doc
  (env : Lean.Environment) (tactic : Lean.Name) : Array String
• Lean.Parser.Tactic.Doc.tacticDocExtExt 📋 Lean.Parser.Tactic.Doc
  : Lean.PersistentEnvExtension (Lean.Name × Array String) (Lean.Name × String) (Lean.NameMap (Array String))
• Lean.Parser.Tactic.Doc.tagInfo 📋 Lean.Parser.Tactic.Doc
  {m : Type → Type} [Monad m] [Lean.MonadEnv m] (tag : Lean.Name) : m (Option (String × Option String))
• Lean.Parser.Tactic.Doc.allTagsWithInfo 📋 Lean.Parser.Tactic.Doc
  {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (List (Lean.Name × String × Option String))
• Lean.Parser.Tactic.Doc.knownTacticTagExt 📋 Lean.Parser.Tactic.Doc
  : Lean.PersistentEnvExtension (Lean.Name × String × Option String) (Lean.Name × String × Option String) (Lean.NameMap (String × Option String))
• Lean.findDocString? 📋 Lean.DocString
  (env : Lean.Environment) (declName : Lean.Name) (includeBuiltin : Bool := true) : IO (Option String)
• Lean.Meta.Simp.mkSimprocAttr 📋 Lean.Meta.Tactic.Simp.Simproc
  (attrName : Lean.Name) (attrDescr : String) (ext : Lean.Meta.Simp.SimprocExtension) (name : Lean.Name) : IO Unit
• Lean.Meta.Simp.registerSimprocAttr 📋 Lean.Meta.Tactic.Simp.Simproc
  (attrName : Lean.Name) (attrDescr : String) (ref? : Option (IO.Ref Lean.Meta.Simprocs)) (name : Lean.Name := by exact decl_name%) : IO Lean.Meta.Simp.SimprocExtension
• Lean.Meta.registerSimpAttr 📋 Lean.Meta.Tactic.Simp.Attr
  (attrName : Lean.Name) (attrDescr : String) (ref : Lean.Name := by exact decl_name%) : IO Lean.Meta.SimpExtension
• Lean.Meta.mkSimpAttr 📋 Lean.Meta.Tactic.Simp.Attr
  (attrName : Lean.Name) (attrDescr : String) (ext : Lean.Meta.SimpExtension) (ref : Lean.Name := by exact decl_name%) : IO Unit
• Lean.Elab.Command.Scope.mk 📋 Lean.Elab.Command
  (header : String) (opts : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (levelNames : List Lean.Name) (varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (varUIds : Array Lean.Name) (includedVars omittedVars : List Lean.Name) (isNoncomputable isPublic : Bool) (attrs : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) : Lean.Elab.Command.Scope
• Lean.Elab.Command.Scope.mk.injEq 📋 Lean.Elab.Command
  (header : String) (opts : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (levelNames : List Lean.Name) (varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (varUIds : Array Lean.Name) (includedVars omittedVars : List Lean.Name) (isNoncomputable isPublic : Bool) (attrs : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) (header✝ : String) (opts✝ : Lean.Options) (currNamespace✝ : Lean.Name) (openDecls✝ : List Lean.OpenDecl) (levelNames✝ : List Lean.Name) (varDecls✝ : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (varUIds✝ : Array Lean.Name) (includedVars✝ omittedVars✝ : List Lean.Name) (isNoncomputable✝ isPublic✝ : Bool) (attrs✝ : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) : ({ header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls, levelNames := levelNames, varDecls := varDecls, varUIds := varUIds, includedVars := includedVars, omittedVars := omittedVars, isNoncomputable := isNoncomputable, isPublic := isPublic, attrs := attrs } = { header := header✝, opts := opts✝, currNamespace := currNamespace✝, openDecls := openDecls✝, levelNames := levelNames✝, varDecls := varDecls✝, varUIds := varUIds✝, includedVars := includedVars✝, omittedVars := omittedVars✝, isNoncomputable := isNoncomputable✝, isPublic := isPublic✝, attrs := attrs✝ }) = (header = header✝ ∧ opts = opts✝ ∧ currNamespace = currNamespace✝ ∧ openDecls = openDecls✝ ∧ levelNames = levelNames✝ ∧ varDecls = varDecls✝ ∧ varUIds = varUIds✝ ∧ includedVars = includedVars✝ ∧ omittedVars = omittedVars✝ ∧ isNoncomputable = isNoncomputable✝ ∧ isPublic = isPublic✝ ∧ attrs = attrs✝)
• Lean.Elab.Command.Scope.mk.sizeOf_spec 📋 Lean.Elab.Command
  (header : String) (opts : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (levelNames : List Lean.Name) (varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (varUIds : Array Lean.Name) (includedVars omittedVars : List Lean.Name) (isNoncomputable isPublic : Bool) (attrs : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) : sizeOf { header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls, levelNames := levelNames, varDecls := varDecls, varUIds := varUIds, includedVars := includedVars, omittedVars := omittedVars, isNoncomputable := isNoncomputable, isPublic := isPublic, attrs := attrs } = 1 + sizeOf header + sizeOf opts + sizeOf currNamespace + sizeOf openDecls + sizeOf levelNames + sizeOf varDecls + sizeOf varUIds + sizeOf includedVars + sizeOf omittedVars + sizeOf isNoncomputable + sizeOf isPublic + sizeOf attrs
• Batteries.Tactic.Lint.formatLinterResults 📋 Batteries.Tactic.Lint.Frontend
  (results : Array (Batteries.Tactic.Lint.NamedLinter × Std.HashMap Lean.Name Lean.MessageData)) (decls : Array Lean.Name) (groupByFilename : Bool) (whereDesc : String) (runSlowLinters : Bool) (verbose : Batteries.Tactic.Lint.LintVerbosity) (numLinters : ℕ) (useErrorFormat : Bool := false) : Lean.CoreM Lean.MessageData
• Lean.Server.FileWorker.applyEditToHint? 📋 Lean.Server.FileWorker.InlayHints
  (hintMod : Lean.Name) (ihi : Lean.Elab.InlayHintInfo) (range : String.Range) (newText : String) : Option Lean.Elab.InlayHintInfo
• Lean.Elab.Tactic.Doc.TacticDoc.mk 📋 Lean.Elab.Tactic.Doc
  (internalName : Lean.Name) (userName : String) (tags : Lean.NameSet) (docString : Option String) (extensionDocs : Array String) : Lean.Elab.Tactic.Doc.TacticDoc
• Lean.Elab.Tactic.Doc.TacticDoc.mk.injEq 📋 Lean.Elab.Tactic.Doc
  (internalName : Lean.Name) (userName : String) (tags : Lean.NameSet) (docString : Option String) (extensionDocs : Array String) (internalName✝ : Lean.Name) (userName✝ : String) (tags✝ : Lean.NameSet) (docString✝ : Option String) (extensionDocs✝ : Array String) : ({ internalName := internalName, userName := userName, tags := tags, docString := docString, extensionDocs := extensionDocs } = { internalName := internalName✝, userName := userName✝, tags := tags✝, docString := docString✝, extensionDocs := extensionDocs✝ }) = (internalName = internalName✝ ∧ userName = userName✝ ∧ tags = tags✝ ∧ docString = docString✝ ∧ extensionDocs = extensionDocs✝)
• Lean.Elab.Tactic.Doc.TacticDoc.mk.sizeOf_spec 📋 Lean.Elab.Tactic.Doc
  (internalName : Lean.Name) (userName : String) (tags : Lean.NameSet) (docString : Option String) (extensionDocs : Array String) : sizeOf { internalName := internalName, userName := userName, tags := tags, docString := docString, extensionDocs := extensionDocs } = 1 + sizeOf internalName + sizeOf userName + sizeOf tags + sizeOf docString + sizeOf extensionDocs
• Batteries.CodeAction.mkTacticCodeAction.unsafe_1 📋 Batteries.CodeAction.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Batteries.CodeAction.TacticCodeAction
• Batteries.CodeAction.mkTacticCodeAction.unsafe_impl_3 📋 Batteries.CodeAction.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Batteries.CodeAction.TacticCodeAction
• Batteries.CodeAction.mkTacticSeqCodeAction.unsafe_1 📋 Batteries.CodeAction.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Batteries.CodeAction.TacticSeqCodeAction
• Batteries.CodeAction.mkTacticSeqCodeAction.unsafe_impl_3 📋 Batteries.CodeAction.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Batteries.CodeAction.TacticSeqCodeAction
• Lean.Compiler.setImplementedBy 📋 Lean.Compiler.ImplementedByAttr
  (env : Lean.Environment) (declName impName : Lean.Name) : Except String Lean.Environment
• Lean.CodeAction.mkCommandCodeAction.unsafe_1 📋 Lean.Server.CodeActions.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Lean.CodeAction.CommandCodeAction
• Lean.CodeAction.mkCommandCodeAction.unsafe_impl_3 📋 Lean.Server.CodeActions.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Lean.CodeAction.CommandCodeAction
• Lean.CodeAction.mkHoleCodeAction.unsafe_1 📋 Lean.Server.CodeActions.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Lean.CodeAction.HoleCodeAction
• Lean.CodeAction.mkHoleCodeAction.unsafe_impl_3 📋 Lean.Server.CodeActions.Attr
  (n : Lean.Name) (env : Lean.Environment) (opts : Lean.Options) : ExceptT String Id Lean.CodeAction.HoleCodeAction
• Batteries.CodeAction.holeKindToHoleString 📋 Batteries.CodeAction.Misc
  (elaborator : Lean.Name) (synthName : String) : String
• Lean.ParametricAttributeExtra.setParam 📋 Batteries.Lean.AttributeExtra
  {α : Type} (attr : Lean.ParametricAttributeExtra α) (env : Lean.Environment) (decl : Lean.Name) (param : α) : Except String Lean.Environment
• Lean.registerTagAttributeExtra 📋 Batteries.Lean.AttributeExtra
  (name : Lean.Name) (descr : String) (extra : List Lean.Name) (validate : Lean.Name → Lean.AttrM Unit := fun x => pure ()) (ref : Lean.Name := by exact decl_name%) : IO Lean.TagAttributeExtra
• String.reduceBinPred 📋 Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
  (declName : Lean.Name) (arity : ℕ) (op : String → String → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step
• String.reduceBoolPred 📋 Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
  (declName : Lean.Name) (arity : ℕ) (op : String → String → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep
• 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.expandNoKindMacroRulesAux 📋 Lean.Elab.Syntax
  (alts : Array (Lean.TSyntax `Lean.Parser.Term.matchAlt)) (cmdName : String) (mkCmd : Option Lean.Name → Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → Lean.Elab.Command.CommandElabM Lean.Command) : Lean.Elab.Command.CommandElabM Lean.Command
• Lean.Server.evalRpcProcedure 📋 Lean.Server.Rpc.RequestHandling
  (env : Lean.Environment) (opts : Lean.Options) (procName : Lean.Name) : Except String Lean.Server.RpcProcedure✝
• Batteries.Tactic.DiscrTreeCache.mk 📋 Batteries.Util.Cache
  {α : Type} [BEq α] (profilingName : String) (processDecl : Lean.Name → Lean.ConstantInfo → Lean.MetaM (Array (Array Lean.Meta.DiscrTree.Key × α))) (post? : Option (Array α → Array α) := none) (init : Lean.MetaM (Lean.Meta.DiscrTree α) := failure) : IO (Batteries.Tactic.DiscrTreeCache α)
• Batteries.Tactic.DeclCache.mk 📋 Batteries.Util.Cache
  {α : Type} (profilingName : String) (pre : Lean.MetaM α := failure) (empty : α) (addDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) (addLibraryDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α := addDecl) (post : α → Lean.MetaM α := fun a => pure a) : IO (Batteries.Tactic.DeclCache α)
• Lean.ParseImports.moduleIdent.parse 📋 Lean.Elab.ParseImportsFast
  (input : String) (finalize : Lean.Name → Lean.ParseImports.Parser) (module : Lean.Name) (s : Lean.ParseImports.State) : Lean.ParseImports.State
• 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.Elab.sortDeclLevelParams 📋 Lean.Elab.DeclUtil
  (scopeParams allUserParams : List Lean.Name) (usedParams : Array Lean.Name) : Except String (List 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.projectionsInfo 📋 Mathlib.Tactic.Simps.Basic
  (l : List Simps.ProjectionData) (pref : String) (str : Lean.Name) : Lean.MessageData
• Simps.getCompositeOfProjections 📋 Mathlib.Tactic.Simps.Basic
  (structName : Lean.Name) (proj : String) : Lean.MetaM (Lean.Expr × Array ℕ)
• Simps.Config.mk 📋 Mathlib.Tactic.Simps.Basic
  (isSimp : Bool) (attrs : List Lean.Name) (simpRhs : Bool) (typeMd rhsMd : Lean.Meta.TransparencyMode) (fullyApplied : Bool) (notRecursive : List Lean.Name) (debug : Bool) (nameStem : Option String) : Simps.Config
• Simps.addProjections 📋 Mathlib.Tactic.Simps.Basic
  (ref : Lean.Syntax) (univs : List Lean.Name) (nm : NameStruct✝) (type lhs rhs : Lean.Expr) (args : Array Lean.Expr) (mustBeStr : Bool) (cfg : Simps.Config) (todo : List (String × Lean.Syntax)) (toApply : List ℕ) : Lean.MetaM (Array Lean.Name)
• simpsTac 📋 Mathlib.Tactic.Simps.Basic
  (ref : Lean.Syntax) (nm : Lean.Name) (cfg : Simps.Config := { }) (todo : List (String × Lean.Syntax) := []) (trc : Bool := false) : Lean.AttrM (Array Lean.Name)
• Simps.Config.mk.injEq 📋 Mathlib.Tactic.Simps.Basic
  (isSimp : Bool) (attrs : List Lean.Name) (simpRhs : Bool) (typeMd rhsMd : Lean.Meta.TransparencyMode) (fullyApplied : Bool) (notRecursive : List Lean.Name) (debug : Bool) (nameStem : Option String) (isSimp✝ : Bool) (attrs✝ : List Lean.Name) (simpRhs✝ : Bool) (typeMd✝ rhsMd✝ : Lean.Meta.TransparencyMode) (fullyApplied✝ : Bool) (notRecursive✝ : List Lean.Name) (debug✝ : Bool) (nameStem✝ : Option String) : ({ isSimp := isSimp, attrs := attrs, simpRhs := simpRhs, typeMd := typeMd, rhsMd := rhsMd, fullyApplied := fullyApplied, notRecursive := notRecursive, debug := debug, nameStem := nameStem } = { isSimp := isSimp✝, attrs := attrs✝, simpRhs := simpRhs✝, typeMd := typeMd✝, rhsMd := rhsMd✝, fullyApplied := fullyApplied✝, notRecursive := notRecursive✝, debug := debug✝, nameStem := nameStem✝ }) = (isSimp = isSimp✝ ∧ attrs = attrs✝ ∧ simpRhs = simpRhs✝ ∧ typeMd = typeMd✝ ∧ rhsMd = rhsMd✝ ∧ fullyApplied = fullyApplied✝ ∧ notRecursive = notRecursive✝ ∧ debug = debug✝ ∧ nameStem = nameStem✝)
• Simps.Config.mk.sizeOf_spec 📋 Mathlib.Tactic.Simps.Basic
  (isSimp : Bool) (attrs : List Lean.Name) (simpRhs : Bool) (typeMd rhsMd : Lean.Meta.TransparencyMode) (fullyApplied : Bool) (notRecursive : List Lean.Name) (debug : Bool) (nameStem : Option String) : sizeOf { isSimp := isSimp, attrs := attrs, simpRhs := simpRhs, typeMd := typeMd, rhsMd := rhsMd, fullyApplied := fullyApplied, notRecursive := notRecursive, debug := debug, nameStem := nameStem } = 1 + sizeOf isSimp + sizeOf attrs + sizeOf simpRhs + sizeOf typeMd + sizeOf rhsMd + sizeOf fullyApplied + sizeOf notRecursive + sizeOf debug + sizeOf nameStem
• ToAdditive.Config.mk 📋 Mathlib.Tactic.ToAdditive.Frontend
  (trace : Bool) (tgt : Lean.Name) (doc : Option String) (allowAutoName : Bool) (reorder : List (List ℕ)) (attrs : Array Lean.Syntax) (ref : Lean.Syntax) (existing : Option Bool) : ToAdditive.Config
• ToAdditive.additivizeLemmas 📋 Mathlib.Tactic.ToAdditive.Frontend
  {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] (names : Array Lean.Name) (desc : String) (t : Lean.Name → m (Array Lean.Name)) : m Unit
• ToAdditive.Config.mk.injEq 📋 Mathlib.Tactic.ToAdditive.Frontend
  (trace : Bool) (tgt : Lean.Name) (doc : Option String) (allowAutoName : Bool) (reorder : List (List ℕ)) (attrs : Array Lean.Syntax) (ref : Lean.Syntax) (existing : Option Bool) (trace✝ : Bool) (tgt✝ : Lean.Name) (doc✝ : Option String) (allowAutoName✝ : Bool) (reorder✝ : List (List ℕ)) (attrs✝ : Array Lean.Syntax) (ref✝ : Lean.Syntax) (existing✝ : Option Bool) : ({ trace := trace, tgt := tgt, doc := doc, allowAutoName := allowAutoName, reorder := reorder, attrs := attrs, ref := ref, existing := existing } = { trace := trace✝, tgt := tgt✝, doc := doc✝, allowAutoName := allowAutoName✝, reorder := reorder✝, attrs := attrs✝, ref := ref✝, existing := existing✝ }) = (trace = trace✝ ∧ tgt = tgt✝ ∧ doc = doc✝ ∧ allowAutoName = allowAutoName✝ ∧ reorder = reorder✝ ∧ attrs = attrs✝ ∧ ref = ref✝ ∧ existing = existing✝)
• ToAdditive.Config.mk.sizeOf_spec 📋 Mathlib.Tactic.ToAdditive.Frontend
  (trace : Bool) (tgt : Lean.Name) (doc : Option String) (allowAutoName : Bool) (reorder : List (List ℕ)) (attrs : Array Lean.Syntax) (ref : Lean.Syntax) (existing : Option Bool) : sizeOf { trace := trace, tgt := tgt, doc := doc, allowAutoName := allowAutoName, reorder := reorder, attrs := attrs, ref := ref, existing := existing } = 1 + sizeOf trace + sizeOf tgt + sizeOf doc + sizeOf allowAutoName + sizeOf reorder + sizeOf attrs + sizeOf ref + sizeOf existing
• Lean.registerLabelAttr 📋 Lean.LabelAttribute
  (attrName : Lean.Name) (attrDescr : String) (ref : Lean.Name := by exact decl_name%) : IO Lean.LabelExtension
• Lean.mkLabelAttr 📋 Lean.LabelAttribute
  (attrName : Lean.Name) (attrDescr : String) (ext : Lean.LabelExtension) (ref : Lean.Name := by exact decl_name%) : IO Unit
• 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
• Lean.IR.emitC 📋 Lean.Compiler.IR.EmitC
  (env : Lean.Environment) (modName : Lean.Name) : Except String String
• Lean.Compiler.LCNF.instantiateForall.go.eq_def 📋 Lean.Compiler.LCNF.Types
  (ps : Array Lean.Expr) (i : ℕ) (type : Lean.Expr) : Lean.Compiler.LCNF.instantiateForall.go ps i type = if h : i < ps.size then match type.headBeta with | Lean.Expr.forallE binderName binderType b binderInfo => Lean.Compiler.LCNF.instantiateForall.go ps (i + 1) (b.instantiate1 ps[i]) | x => Lean.throwError (Lean.toMessageData "invalid instantiateForall, too many parameters") else pure type
• Lean.IR.getCtorLayout 📋 Lean.Compiler.IR.ToIRType
  (env : Lean.Environment) (ctorName : Lean.Name) : Except String Lean.IR.CtorLayout
• Lean.IR.emitLLVM 📋 Lean.Compiler.IR.EmitLLVM
  (env : Lean.Environment) (modName : Lean.Name) (filepath : String) : IO Unit
• 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.IR.EmitLLVM.callModInitFn 📋 Lean.Compiler.IR.EmitLLVM
  {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (modName : Lean.Name) (input world : LLVM.Value llvmctx) (retName : String) : Lean.IR.EmitLLVM.M llvmctx (LLVM.Value llvmctx)
• Lean.Compiler.LCNF.Testing.assertDoesNotContainConstAfter 📋 Lean.Compiler.LCNF.Testing
  (constName : Lean.Name) (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller
• Lean.Meta.ArgsPacker.Mutual.mkCodomain.go.eq_def 📋 Lean.Meta.ArgsPacker
  (types : Array Lean.Expr) (u : Lean.Level) (x : Lean.Expr) (i : ℕ) : Lean.Meta.ArgsPacker.Mutual.mkCodomain.go types u x i = if i < types.size - 1 then do let __do_lift ← Lean.Meta.inferType x let xType ← Lean.Meta.whnfD __do_lift if xType.isAppOfArity `PSum 2 = true then have xTypeArgs := xType.getAppArgs; have casesOn := Lean.mkConst `PSum.casesOn (Lean.mkLevelSucc u :: xType.getAppFn.constLevels!); have casesOn := Lean.mkAppN casesOn xTypeArgs; do let __do_lift ← Lean.Meta.mkLambdaFVars #[x] (Lean.mkSort u) have casesOn : Lean.Expr := Lean.mkApp casesOn __do_lift have casesOn : Lean.Expr := Lean.mkApp casesOn x let __do_lift ← liftM (Lean.mkFreshUserName `_x) let minor1 ← Lean.Meta.withLocalDeclD __do_lift xTypeArgs[0]! fun x => Lean.Meta.mkLambdaFVars #[x] (types[i]!.bindingBody!.instantiate1 x) let __do_lift ← liftM (Lean.mkFreshUserName `_x) let minor2 ← Lean.Meta.withLocalDeclD __do_lift xTypeArgs[1]! fun x => do let __do_lift ← Lean.Meta.ArgsPacker.Mutual.mkCodomain.go types u x (i + 1) Lean.Meta.mkLambdaFVars #[x] __do_lift pure (Lean.mkApp2 casesOn minor1 minor2) else panicWithPosWithDecl "Lean.Meta.ArgsPacker" "Lean.Meta.ArgsPacker.Mutual.mkCodomain.go" 312 6 ("assertion violation: " ++ "xType.isAppOfArity ``PSum 2\n ") else pure (types[i]!.bindingBody!.instantiate1 x)
• Lean.Elab.Term.Quotation.resolveSectionVariable 📋 Lean.Elab.Quotation
  (sectionVars : Lean.NameMap Lean.Name) (id : Lean.Name) : List (Lean.Name × List String)
• Lean.Elab.Term.Quotation.resolveSectionVariable.loop 📋 Lean.Elab.Quotation
  (sectionVars : Lean.NameMap Lean.Name) (extractionResult : Lean.MacroScopesView) : Lean.Name → List String → List (Lean.Name × List String)
• Lean.Firefox.Category.mk 📋 Lean.Util.Profiler
  (name : Lean.Name) (color : String) (subcategories : Array String) : Lean.Firefox.Category

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