Loogle!
Result
Found 221 definitions mentioning String and Lean.Name. Of these, only the first 200 are shown.
- Lean.Name.mkSimple Init.Prelude
String → Lean.Name - Lean.Name.mkStr1 Init.Prelude
String → Lean.Name - Lean.Name.mkStr Init.Prelude
Lean.Name → String → Lean.Name - Lean.Name.mkStr2 Init.Prelude
String → String → Lean.Name - Lean.Name.str Init.Prelude
Lean.Name → String → Lean.Name - Lean.Macro.trace Init.Prelude
Lean.Name → String → Lean.MacroM Unit - Lean.Name.mkStr3 Init.Prelude
String → String → String → Lean.Name - Lean.Syntax.Preresolved.decl Init.Prelude
Lean.Name → List String → Lean.Syntax.Preresolved - Lean.Name.mkStr4 Init.Prelude
String → String → String → String → Lean.Name - Lean.Macro.State.traceMsgs Init.Prelude
Lean.Macro.State → List (Lean.Name × String) - Lean.Name.mkStr5 Init.Prelude
String → String → String → String → String → Lean.Name - Lean.Macro.State.mk Init.Prelude
Lean.MacroScope → List (Lean.Name × String) → Lean.Macro.State - Lean.Macro.resolveGlobalName Init.Prelude
Lean.Name → Lean.MacroM (List (Lean.Name × List String)) - Lean.Name.mkStr6 Init.Prelude
String → String → String → String → String → String → Lean.Name - Lean.Name.mkStr7 Init.Prelude
String → String → String → String → String → String → String → Lean.Name - Lean.Macro.Methods.resolveGlobalName Init.Prelude
Lean.Macro.Methods → Lean.Name → Lean.MacroM (List (Lean.Name × List String)) - Lean.Name.mkStr8 Init.Prelude
String → String → String → String → String → String → String → String → Lean.Name - Lean.Macro.Methods.mk Init.Prelude
(Lean.Syntax → Lean.MacroM (Option Lean.Syntax)) → Lean.MacroM Lean.Name → (Lean.Name → Lean.MacroM Bool) → (Lean.Name → Lean.MacroM (List Lean.Name)) → (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_1 : Lean.Name) (str_1 : String), (pre.str str = pre_1.str str_1) = (pre = pre_1 ∧ str = str_1) - String.toName Init.Meta
String → Lean.Name - Lean.Name.appendAfter Init.Meta
Lean.Name → String → Lean.Name - Lean.Name.appendBefore Init.Meta
Lean.Name → String → Lean.Name - Lean.Syntax.decodeNameLit Init.Meta
String → Option Lean.Name - Lean.Name.toStringWithSep Init.Meta
String → Bool → Lean.Name → String - Lean.Name.toString Init.Meta
Lean.Name → optParam Bool true → String - Lean.Name.beq.eq_2 Init.Meta
∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), (p₁.str s₁).beq (p₂.str s₂) = (s₁ == s₂ && p₁.beq p₂) - Lean.Name.beq.eq_4 Init.Meta
∀ (x x_1 : Lean.Name), (x = Lean.Name.anonymous → x_1 = Lean.Name.anonymous → False) → (∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), x = p₁.str s₁ → x_1 = p₂.str s₂ → False) → (∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), x = p₁.num n₁ → x_1 = p₂.num n₂ → False) → x.beq x_1 = false - Lean.KVMap.setString Lean.Data.KVMap
Lean.KVMap → Lean.Name → String → Lean.KVMap - Lean.KVMap.updateString Lean.Data.KVMap
Lean.KVMap → Lean.Name → (String → String) → Lean.KVMap - Lean.KVMap.getString Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam 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
Lean.Name → (String → Bool) → Bool - Lean.getOptionDescr Lean.Data.Options
Lean.Name → IO String - Lean.OptionDecl.mk Lean.Data.Options
autoParam Lean.Name _auto✝ → Lean.DataValue → String → String → Lean.OptionDecl - Lean.OptionDecl.mk.injEq Lean.Data.Options
∀ (declName : autoParam Lean.Name _auto✝) (defValue : Lean.DataValue) (group descr : String) (declName_1 : autoParam Lean.Name _auto✝) (defValue_1 : Lean.DataValue) (group_1 descr_1 : String), ({ declName := declName, defValue := defValue, group := group, descr := descr } = { declName := declName_1, defValue := defValue_1, group := group_1, descr := descr_1 }) = (declName = declName_1 ∧ defValue = defValue_1 ∧ group = group_1 ∧ descr = descr_1) - Lean.OptionDecl.mk.sizeOf_spec Lean.Data.Options
∀ (declName : autoParam Lean.Name _auto✝) (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
Lean.Format → optParam Lean.Options { entries := [] } → String - Lean.modToFilePath Lean.Util.Path
System.FilePath → Lean.Name → String → System.FilePath - Lean.SearchPath.findModuleWithExt Lean.Util.Path
Lean.SearchPath → String → Lean.Name → IO (Option System.FilePath) - Lean.SearchPath.findWithExt Lean.Util.Path
Lean.SearchPath → String → Lean.Name → IO (Option System.FilePath) - Lean.forEachModuleInDir Lean.Util.Path
{m : Type → Type u_1} → [inst : Monad m] → [inst : MonadLiftT IO m] → System.FilePath → (Lean.Name → m PUnit.{1}) → optParam String "lean" → m PUnit.{1} - Lean.profileit Lean.Util.Profile
{α : Type} → String → Lean.Options → (Unit → α) → optParam Lean.Name Lean.Name.anonymous → α - Lean.profileitIO Lean.Util.Profile
{ε α : Type} → String → Lean.Options → EIO ε α → optParam Lean.Name Lean.Name.anonymous → EIO ε α - Lean.profileitIOUnsafe Lean.Util.Profile
{ε α : Type} → String → Lean.Options → EIO ε α → optParam Lean.Name Lean.Name.anonymous → EIO ε α - Lean.profileitM Lean.Util.Profile
{m : Type → Type} → (ε : Type) → [inst : MonadFunctorT (EIO ε) m] → {α : Type} → String → Lean.Options → m α → optParam Lean.Name Lean.Name.anonymous → m α - Lean.Environment.evalConst Lean.Environment
(α : Type u_1) → Lean.Environment → Lean.Options → Lean.Name → Except String α - Lean.Environment.evalConstCheck Lean.Environment
(α : Type) → Lean.Environment → Lean.Options → Lean.Name → Lean.Name → ExceptT String Id α - Lean.Json.parseTagged Lean.Data.Json.FromToJson
Lean.Json → String → ℕ → Option (Array Lean.Name) → Except String (Array Lean.Json) - Lean.Syntax.mkAntiquotNode Lean.Syntax
Lean.Name → Lean.Syntax → optParam ℕ 0 → optParam (Option String) none → optParam Bool false → Lean.Syntax - Lean.TraceData.mk Lean.Message
Lean.Name → Float → Float → Bool → String → Lean.TraceData - Lean.TraceData.mk.injEq Lean.Message
∀ (cls : Lean.Name) (startTime stopTime : Float) (collapsed : Bool) (tag : String) (cls_1 : Lean.Name) (startTime_1 stopTime_1 : Float) (collapsed_1 : Bool) (tag_1 : String), ({ cls := cls, startTime := startTime, stopTime := stopTime, collapsed := collapsed, tag := tag } = { cls := cls_1, startTime := startTime_1, stopTime := stopTime_1, collapsed := collapsed_1, tag := tag_1 }) = (cls = cls_1 ∧ startTime = startTime_1 ∧ stopTime = stopTime_1 ∧ collapsed = collapsed_1 ∧ tag = tag_1) - 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} → [inst : Monad m] → [inst : Lean.MonadTrace m] → [inst : MonadLiftT IO m] → [inst : Lean.MonadRef m] → [inst : Lean.AddMessageContext m] → [inst : Lean.MonadOptions m] → [inst : Lean.MonadAlwaysExcept Lean.Exception m] → [inst : MonadLiftT BaseIO m] → Lean.Name → m (α × Lean.MessageData) → optParam Bool true → optParam String "" → m α - Lean.withTraceNode Lean.Util.Trace
{α : Type} → {m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadTrace m] → [inst : MonadLiftT IO m] → [inst : Lean.MonadRef m] → [inst : Lean.AddMessageContext m] → [inst : Lean.MonadOptions m] → {ε : Type} → [always : Lean.MonadAlwaysExcept ε m] → [inst : MonadLiftT BaseIO m] → Lean.Name → (Except ε α → m Lean.MessageData) → m α → optParam Bool true → optParam String "" → m α - Lean.withTraceNodeBefore Lean.Util.Trace
{α : Type} → {m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadTrace m] → [inst : MonadLiftT IO m] → {ε : Type} → [inst : Lean.MonadRef m] → [inst : Lean.AddMessageContext m] → [inst : Lean.MonadOptions m] → [always : Lean.MonadAlwaysExcept ε m] → [inst : MonadLiftT BaseIO m] → [inst : Lean.ExceptToEmoji ε α] → Lean.Name → m Lean.MessageData → m α → optParam Bool true → optParam String "" → m α - Lean.ResolveName.resolveGlobalName Lean.ResolveName
Lean.Environment → Lean.Name → List Lean.OpenDecl → Lean.Name → List (Lean.Name × List String) - Lean.ensureReservedNameAvailable Lean.ResolveName
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadEnv m] → [inst : Lean.MonadError m] → Lean.Name → String → m Unit - 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.filterFieldList Lean.ResolveName
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadError m] → Lean.Name → List (Lean.Name × List String) → m (List Lean.Name) - Lean.resolveGlobalName Lean.ResolveName
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadResolveName m] → [inst : Lean.MonadEnv m] → Lean.Name → m (List (Lean.Name × List String)) - Lean.isAuxRecursorWithSuffix Lean.AuxRecursor
Lean.Environment → Lean.Name → String → Bool - Lean.Compiler.checkIsDefinition Lean.Compiler.Old
Lean.Environment → Lean.Name → Except String Unit - Lean.Core.checkMaxHeartbeatsCore Lean.CoreM
String → Lean.Name → ℕ → Lean.CoreM Unit - Lean.Core.Context.mk Lean.CoreM
String → Lean.FileMap → Lean.Options → ℕ → ℕ → Lean.Syntax → Lean.Name → List Lean.OpenDecl → ℕ → ℕ → Lean.MacroScope → Bool → Bool → 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) (catchRuntimeEx diag : Bool) (fileName_1 : String) (fileMap_1 : Lean.FileMap) (options_1 : Lean.Options) (currRecDepth_1 maxRecDepth_1 : ℕ) (ref_1 : Lean.Syntax) (currNamespace_1 : Lean.Name) (openDecls_1 : List Lean.OpenDecl) (initHeartbeats_1 maxHeartbeats_1 : ℕ) (currMacroScope_1 : Lean.MacroScope) (catchRuntimeEx_1 diag_1 : Bool), ({ fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls, initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, currMacroScope := currMacroScope, catchRuntimeEx := catchRuntimeEx, diag := diag } = { fileName := fileName_1, fileMap := fileMap_1, options := options_1, currRecDepth := currRecDepth_1, maxRecDepth := maxRecDepth_1, ref := ref_1, currNamespace := currNamespace_1, openDecls := openDecls_1, initHeartbeats := initHeartbeats_1, maxHeartbeats := maxHeartbeats_1, currMacroScope := currMacroScope_1, catchRuntimeEx := catchRuntimeEx_1, diag := diag_1 }) = (fileName = fileName_1 ∧ fileMap = fileMap_1 ∧ options = options_1 ∧ currRecDepth = currRecDepth_1 ∧ maxRecDepth = maxRecDepth_1 ∧ ref = ref_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ initHeartbeats = initHeartbeats_1 ∧ maxHeartbeats = maxHeartbeats_1 ∧ currMacroScope = currMacroScope_1 ∧ catchRuntimeEx = catchRuntimeEx_1 ∧ diag = diag_1) - 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) (catchRuntimeEx diag : Bool), sizeOf { fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls, initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, currMacroScope := currMacroScope, catchRuntimeEx := catchRuntimeEx, diag := diag } = 1 + sizeOf fileName + sizeOf fileMap + sizeOf options + sizeOf currRecDepth + sizeOf maxRecDepth + sizeOf ref + sizeOf currNamespace + sizeOf openDecls + sizeOf initHeartbeats + sizeOf maxHeartbeats + sizeOf currMacroScope + sizeOf catchRuntimeEx + sizeOf diag - Lean.getAttributeImpl Lean.Attributes
Lean.Environment → Lean.Name → Except String Lean.AttributeImpl - Lean.mkAttributeImplOfConstant Lean.Attributes
Lean.Environment → Lean.Options → Lean.Name → Except String Lean.AttributeImpl - Lean.mkAttributeImplOfConstantUnsafe Lean.Attributes
Lean.Environment → Lean.Options → Lean.Name → Except String Lean.AttributeImpl - Lean.registerAttributeOfDecl Lean.Attributes
Lean.Environment → Lean.Options → Lean.Name → Except String Lean.Environment - Lean.AttributeImplCore.mk Lean.Attributes
autoParam Lean.Name _auto✝ → Lean.Name → String → Lean.AttributeApplicationTime → Lean.AttributeImplCore - Lean.EnumAttributes.setValue Lean.Attributes
{α : Type} → Lean.EnumAttributes α → Lean.Environment → Lean.Name → α → Except String Lean.Environment - Lean.ParametricAttribute.setParam Lean.Attributes
{α : Type} → Lean.ParametricAttribute α → Lean.Environment → Lean.Name → α → Except String Lean.Environment - Lean.registerTagAttribute Lean.Attributes
Lean.Name → String → (optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) → autoParam Lean.Name _auto✝ → optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking → IO Lean.TagAttribute - Lean.registerEnumAttributes Lean.Attributes
{α : Type} → [inst : Inhabited α] → List (Lean.Name × String × α) → (optParam (Lean.Name → α → Lean.AttrM Unit) fun x x => pure ()) → optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking → autoParam Lean.Name _auto✝ → IO (Lean.EnumAttributes α) - Lean.AttributeImplCore.mk.injEq Lean.Attributes
∀ (ref : autoParam Lean.Name _auto✝) (name : Lean.Name) (descr : String) (applicationTime : Lean.AttributeApplicationTime) (ref_1 : autoParam Lean.Name _auto✝) (name_1 : Lean.Name) (descr_1 : String) (applicationTime_1 : Lean.AttributeApplicationTime), ({ ref := ref, name := name, descr := descr, applicationTime := applicationTime } = { ref := ref_1, name := name_1, descr := descr_1, applicationTime := applicationTime_1 }) = (ref = ref_1 ∧ name = name_1 ∧ descr = descr_1 ∧ applicationTime = applicationTime_1) - Lean.AttributeImplCore.mk.sizeOf_spec Lean.Attributes
∀ (ref : autoParam Lean.Name _auto✝) (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.addClass Lean.Class
Lean.Environment → Lean.Name → Except String Lean.Environment - Lean.Compiler.setInlineAttribute Lean.Compiler.InlineAttrs
Lean.Environment → Lean.Name → Lean.Compiler.InlineAttributeKind → Except String Lean.Environment - Lean.realizeGlobalName Lean.ReservedNameAction
Lean.Name → Lean.CoreM (List (Lean.Name × List String)) - Lean.Elab.realizeGlobalNameWithInfos Lean.Elab.InfoTree.Main
Lean.Syntax → Lean.Name → Lean.CoreM (List (Lean.Name × List String)) - Lean.Linter.DeprecationEntry.mk Lean.Linter.Deprecated
Option Lean.Name → Option String → Option String → Lean.Linter.DeprecationEntry - Lean.Linter.DeprecationEntry.mk.injEq Lean.Linter.Deprecated
∀ (newName? : Option Lean.Name) (text? since? : Option String) (newName?_1 : Option Lean.Name) (text?_1 since?_1 : Option String), ({ newName? := newName?, text? := text?, since? := since? } = { newName? := newName?_1, text? := text?_1, since? := since?_1 }) = (newName? = newName?_1 ∧ text? = text?_1 ∧ since? = since?_1) - 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.setBuiltinInitAttr Lean.Compiler.InitAttr
Lean.Environment → Lean.Name → optParam Lean.Name Lean.Name.anonymous → Except String Lean.Environment - Lean.addBuiltinDocString Lean.DocString
Lean.Name → String → IO Unit - Lean.findDocString? Lean.DocString
Lean.Environment → Lean.Name → optParam Bool true → IO (Option String) - Lean.addDocString Lean.DocString
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadError m] → [inst : Lean.MonadEnv m] → Lean.Name → String → m Unit - Lean.addDocString' Lean.DocString
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadError m] → [inst : Lean.MonadEnv m] → Lean.Name → Option String → m Unit - Lean.Parser.throwUnknownParserCategory Lean.Parser.Extension
{α : Type} → Lean.Name → ExceptT String Id α - Lean.Parser.addParserCategory Lean.Parser.Extension
Lean.Environment → Lean.Name → Lean.Name → Lean.Parser.LeadingIdentBehavior → Except String Lean.Environment - Lean.Parser.addLeadingParser Lean.Parser.Extension
Lean.Parser.ParserCategories → Lean.Name → Lean.Name → Lean.Parser.Parser → ℕ → Except String Lean.Parser.ParserCategories - Lean.Parser.addTrailingParser Lean.Parser.Extension
Lean.Parser.ParserCategories → Lean.Name → Lean.Name → Lean.Parser.TrailingParser → ℕ → Except String Lean.Parser.ParserCategories - Lean.Parser.addParser Lean.Parser.Extension
Lean.Parser.ParserCategories → Lean.Name → Lean.Name → Bool → Lean.Parser.Parser → ℕ → Except String Lean.Parser.ParserCategories - Lean.Parser.runParserCategory Lean.Parser.Extension
Lean.Environment → Lean.Name → String → optParam String "<input>" → Except String Lean.Syntax - Lean.ParserCompiler.registerCombinatorAttribute Lean.ParserCompiler.Attribute
Lean.Name → String → autoParam Lean.Name _auto✝ → IO Lean.ParserCompiler.CombinatorAttribute - Lean.ExternEntry.foreign Lean.Compiler.ExternAttr
Lean.Name → String → Lean.ExternEntry - Lean.ExternEntry.inline Lean.Compiler.ExternAttr
Lean.Name → String → Lean.ExternEntry - Lean.ExternEntry.standard Lean.Compiler.ExternAttr
Lean.Name → String → Lean.ExternEntry - Lean.getExternNameFor Lean.Compiler.ExternAttr
Lean.Environment → Lean.Name → Lean.Name → Option String - Lean.addExtern Lean.Compiler.ExternAttr
Lean.Environment → Lean.Name → ExceptT String Id Lean.Environment - Lean.ExternEntry.foreign.injEq Lean.Compiler.ExternAttr
∀ (backend : Lean.Name) (fn : String) (backend_1 : Lean.Name) (fn_1 : String), (Lean.ExternEntry.foreign backend fn = Lean.ExternEntry.foreign backend_1 fn_1) = (backend = backend_1 ∧ fn = fn_1) - Lean.ExternEntry.inline.injEq Lean.Compiler.ExternAttr
∀ (backend : Lean.Name) (pattern : String) (backend_1 : Lean.Name) (pattern_1 : String), (Lean.ExternEntry.inline backend pattern = Lean.ExternEntry.inline backend_1 pattern_1) = (backend = backend_1 ∧ pattern = pattern_1) - Lean.ExternEntry.standard.injEq Lean.Compiler.ExternAttr
∀ (backend : Lean.Name) (fn : String) (backend_1 : Lean.Name) (fn_1 : String), (Lean.ExternEntry.standard backend fn = Lean.ExternEntry.standard backend_1 fn_1) = (backend = backend_1 ∧ fn = fn_1) - Lean.ExternEntry.foreign.sizeOf_spec Lean.Compiler.ExternAttr
∀ (backend : Lean.Name) (fn : String), sizeOf (Lean.ExternEntry.foreign backend fn) = 1 + sizeOf backend + sizeOf 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} → Lean.Name → Lean.Name → String → Lean.Name → (Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) → (Bool → Lean.Name → Lean.AttrM Unit) → Lean.KeyedDeclsAttribute.Def γ - Lean.KeyedDeclsAttribute.Def.mk.sizeOf_spec Lean.KeyedDeclsAttribute
∀ {γ : Type} [inst : 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_1 name_1 : Lean.Name) (descr_1 : String) (valueTypeName_1 : Lean.Name) (evalKey_1 : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key) (onAdded_1 : Bool → Lean.Name → Lean.AttrM Unit), ({ builtinName := builtinName, name := name, descr := descr, valueTypeName := valueTypeName, evalKey := evalKey, onAdded := onAdded } = { builtinName := builtinName_1, name := name_1, descr := descr_1, valueTypeName := valueTypeName_1, evalKey := evalKey_1, onAdded := onAdded_1 }) = (builtinName = builtinName_1 ∧ name = name_1 ∧ descr = descr_1 ∧ valueTypeName = valueTypeName_1 ∧ evalKey = evalKey_1 ∧ onAdded = onAdded_1) - Lean.Elab.evalSyntaxConstant Lean.Elab.Util
Lean.Environment → Lean.Options → Lean.Name → ExceptT String Id Lean.Syntax - Lean.Elab.mkElabAttribute Lean.Elab.Util
(γ : Type) → Lean.Name → Lean.Name → Lean.Name → Lean.Name → String → autoParam Lean.Name _auto✝ → IO (Lean.KeyedDeclsAttribute γ) - Lean.Elab.Term.LVal.fieldName Lean.Elab.Term
Lean.Syntax → String → Option Lean.Name → Lean.Syntax → Lean.Elab.Term.LVal - Lean.Elab.Term.resolveLocalName Lean.Elab.Term
Lean.Name → Lean.Elab.TermElabM (Option (Lean.Expr × List String)) - Lean.Elab.Term.resolveName.process Lean.Elab.Term
Lean.Name → List Lean.Level → List (Lean.Name × List String) → Lean.Elab.TermElabM (List (Lean.Expr × List String)) - Lean.Elab.Term.resolveLocalName.loop Lean.Elab.Term
Lean.MacroScopesView → (Lean.MacroScopesView → Bool → Option Lean.LocalDecl) → Lean.Name → List String → Bool → Lean.Elab.TermElabM (Option (Lean.Expr × List String)) - Lean.Elab.Term.resolveName Lean.Elab.Term
Lean.Syntax → Lean.Name → List Lean.Syntax.Preresolved → List Lean.Level → optParam (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_1 : Lean.Syntax) (name_1 : String) (suffix?_1 : Option Lean.Name) (fullRef_1 : Lean.Syntax), (Lean.Elab.Term.LVal.fieldName ref name suffix? fullRef = Lean.Elab.Term.LVal.fieldName ref_1 name_1 suffix?_1 fullRef_1) = (ref = ref_1 ∧ name = name_1 ∧ suffix? = suffix?_1 ∧ fullRef = fullRef_1) - 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.appendSection Lean.Meta.Diagnostics
Lean.MessageData → Lean.Name → String → Lean.Meta.DiagSummary → Lean.MessageData - Lean.Elab.Command.Scope.mk Lean.Elab.Command
String → Lean.Options → Lean.Name → List Lean.OpenDecl → List Lean.Name → Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder) → Array Lean.Name → Bool → 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) (isNoncomputable : Bool) (header_1 : String) (opts_1 : Lean.Options) (currNamespace_1 : Lean.Name) (openDecls_1 : List Lean.OpenDecl) (levelNames_1 : List Lean.Name) (varDecls_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (varUIds_1 : Array Lean.Name) (isNoncomputable_1 : Bool), ({ header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls, levelNames := levelNames, varDecls := varDecls, varUIds := varUIds, isNoncomputable := isNoncomputable } = { header := header_1, opts := opts_1, currNamespace := currNamespace_1, openDecls := openDecls_1, levelNames := levelNames_1, varDecls := varDecls_1, varUIds := varUIds_1, isNoncomputable := isNoncomputable_1 }) = (header = header_1 ∧ opts = opts_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ levelNames = levelNames_1 ∧ varDecls = varDecls_1 ∧ varUIds = varUIds_1 ∧ isNoncomputable = isNoncomputable_1) - 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) (isNoncomputable : Bool), sizeOf { header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls, levelNames := levelNames, varDecls := varDecls, varUIds := varUIds, isNoncomputable := isNoncomputable } = 1 + sizeOf header + sizeOf opts + sizeOf currNamespace + sizeOf openDecls + sizeOf levelNames + sizeOf varDecls + sizeOf varUIds + sizeOf isNoncomputable - Mathlib.Prelude.Rename.NameEntry.mk Mathlib.Mathport.Rename
Lean.Name → Lean.Name → Bool → String → Mathlib.Prelude.Rename.NameEntry - Mathlib.Prelude.Rename.RenameMap.toLean4 Mathlib.Mathport.Rename
Mathlib.Prelude.Rename.RenameMap → Lean.NameMap (String × Lean.Name) - Mathlib.Prelude.Rename.ImportEntry.mk Mathlib.Mathport.Rename
Lean.Name → Option (String × String) → Mathlib.Prelude.Rename.ImportEntry - Mathlib.Prelude.Rename.RenameMap.find? Mathlib.Mathport.Rename
Mathlib.Prelude.Rename.RenameMap → Lean.Name → Option (String × Lean.Name) - Mathlib.Prelude.Rename.addNameAlignment Mathlib.Mathport.Rename
Lean.Name → Lean.Name → optParam Bool false → optParam String "" → Lean.CoreM Unit - Mathlib.Prelude.Rename.RenameMap.mk Mathlib.Mathport.Rename
Lean.NameMap (String × Lean.Name) → Lean.NameMap (Lean.Name × List Lean.Name) → Mathlib.Prelude.Rename.RenameMap - Mathlib.Prelude.Rename.ImportEntry.mk.injEq Mathlib.Mathport.Rename
∀ (mod3 : Lean.Name) (origin : Option (String × String)) (mod3_1 : Lean.Name) (origin_1 : Option (String × String)), ({ mod3 := mod3, origin := origin } = { mod3 := mod3_1, origin := origin_1 }) = (mod3 = mod3_1 ∧ origin = origin_1) - Mathlib.Prelude.Rename.NameEntry.mk.injEq Mathlib.Mathport.Rename
∀ (n3 n4 : Lean.Name) (synthetic : Bool) (dubious : String) (n3_1 n4_1 : Lean.Name) (synthetic_1 : Bool) (dubious_1 : String), ({ n3 := n3, n4 := n4, synthetic := synthetic, dubious := dubious } = { n3 := n3_1, n4 := n4_1, synthetic := synthetic_1, dubious := dubious_1 }) = (n3 = n3_1 ∧ n4 = n4_1 ∧ synthetic = synthetic_1 ∧ dubious = dubious_1) - Mathlib.Prelude.Rename.RenameMap.mk.injEq Mathlib.Mathport.Rename
∀ (toLean4 : Lean.NameMap (String × Lean.Name)) (toLean3 : Lean.NameMap (Lean.Name × List Lean.Name)) (toLean4_1 : Lean.NameMap (String × Lean.Name)) (toLean3_1 : Lean.NameMap (Lean.Name × List Lean.Name)), ({ toLean4 := toLean4, toLean3 := toLean3 } = { toLean4 := toLean4_1, toLean3 := toLean3_1 }) = (toLean4 = toLean4_1 ∧ toLean3 = toLean3_1) - Mathlib.Prelude.Rename.ImportEntry.mk.sizeOf_spec Mathlib.Mathport.Rename
∀ (mod3 : Lean.Name) (origin : Option (String × String)), sizeOf { mod3 := mod3, origin := origin } = 1 + sizeOf mod3 + sizeOf origin - Mathlib.Prelude.Rename.RenameMap.mk.sizeOf_spec Mathlib.Mathport.Rename
∀ (toLean4 : Lean.NameMap (String × Lean.Name)) (toLean3 : Lean.NameMap (Lean.Name × List Lean.Name)), sizeOf { toLean4 := toLean4, toLean3 := toLean3 } = 1 + sizeOf toLean4 + sizeOf toLean3 - Mathlib.Prelude.Rename.NameEntry.mk.sizeOf_spec Mathlib.Mathport.Rename
∀ (n3 n4 : Lean.Name) (synthetic : Bool) (dubious : String), sizeOf { n3 := n3, n4 := n4, synthetic := synthetic, dubious := dubious } = 1 + sizeOf n3 + sizeOf n4 + sizeOf synthetic + sizeOf dubious - Lean.CodeAction.mkCommandCodeAction.unsafe_1 Lean.Server.CodeActions.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.CommandCodeAction - Lean.CodeAction.mkCommandCodeAction.unsafe_impl_1 Lean.Server.CodeActions.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.CommandCodeAction - Lean.CodeAction.mkHoleCodeAction.unsafe_1 Lean.Server.CodeActions.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.HoleCodeAction - Lean.CodeAction.mkHoleCodeAction.unsafe_impl_1 Lean.Server.CodeActions.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.HoleCodeAction - Lean.Compiler.setImplementedBy Lean.Compiler.ImplementedByAttr
Lean.Environment → Lean.Name → Lean.Name → Except String Lean.Environment - Std.CodeAction.mkTacticCodeAction.unsafe_1 Batteries.CodeAction.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Std.CodeAction.TacticCodeAction - Std.CodeAction.mkTacticCodeAction.unsafe_impl_1 Batteries.CodeAction.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Std.CodeAction.TacticCodeAction - Std.CodeAction.mkTacticSeqCodeAction.unsafe_1 Batteries.CodeAction.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Std.CodeAction.TacticSeqCodeAction - Std.CodeAction.mkTacticSeqCodeAction.unsafe_impl_1 Batteries.CodeAction.Attr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Std.CodeAction.TacticSeqCodeAction - Lean.Server.evalRpcProcedure Lean.Server.Rpc.RequestHandling
Lean.Environment → Lean.Options → Lean.Name → Except String Lean.Server.RpcProcedure - Lean.Meta.Simp.mkSimprocAttr Lean.Meta.Tactic.Simp.Simproc
Lean.Name → String → Lean.Meta.Simp.SimprocExtension → Lean.Name → IO Unit - Lean.Meta.Simp.registerSimprocAttr Lean.Meta.Tactic.Simp.Simproc
Lean.Name → String → Option (IO.Ref Lean.Meta.Simprocs) → autoParam Lean.Name _auto✝ → IO Lean.Meta.Simp.SimprocExtension - Lean.Meta.registerSimpAttr Lean.Meta.Tactic.Simp.Attr
Lean.Name → String → autoParam Lean.Name _auto✝ → IO Lean.Meta.SimpExtension - Lean.Meta.mkSimpAttr Lean.Meta.Tactic.Simp.Attr
Lean.Name → String → Lean.Meta.SimpExtension → autoParam Lean.Name _auto✝ → IO Unit - Lean.NameMapAttributeImpl.mk Batteries.Lean.NameMapAttribute
{α : Type} → Lean.Name → autoParam Lean.Name _auto✝ → String → (Lean.Name → Lean.Syntax → Lean.AttrM α) → Lean.NameMapAttributeImpl α - Lean.NameMapAttributeImpl.mk.injEq Batteries.Lean.NameMapAttribute
∀ {α : Type} (name : Lean.Name) (ref : autoParam Lean.Name _auto✝) (descr : String) (add : Lean.Name → Lean.Syntax → Lean.AttrM α) (name_1 : Lean.Name) (ref_1 : autoParam Lean.Name _auto✝) (descr_1 : String) (add_1 : Lean.Name → Lean.Syntax → Lean.AttrM α), ({ name := name, ref := ref, descr := descr, add := add } = { name := name_1, ref := ref_1, descr := descr_1, add := add_1 }) = (name = name_1 ∧ ref = ref_1 ∧ descr = descr_1 ∧ add = add_1) - Lean.NameMapAttributeImpl.mk.sizeOf_spec Batteries.Lean.NameMapAttribute
∀ {α : Type} [inst : SizeOf α] (name : Lean.Name) (ref : autoParam Lean.Name _auto✝) (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
Lean.Name → String → String - Lean.Elab.Command.expandNoKindMacroRulesAux Lean.Elab.Syntax
Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → String → (Option Lean.Name → Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → Lean.Elab.Command.CommandElabM Lean.Command) → Lean.Elab.Command.CommandElabM Lean.Command - Std.Tactic.Lint.formatLinterResults Batteries.Tactic.Lint.Frontend
Array (Std.Tactic.Lint.NamedLinter × Lean.HashMap Lean.Name Lean.MessageData) → Array Lean.Name → Bool → String → Bool → Std.Tactic.Lint.LintVerbosity → ℕ → optParam Bool false → Lean.CoreM Lean.MessageData - Lean.Name.getString Mathlib.Lean.Expr.Basic
Lean.Name → String - Lean.Name.lastComponentAsString Mathlib.Lean.Expr.Basic
Lean.Name → String - Lean.Name.updateLast Mathlib.Lean.Expr.Basic
(String → String) → Lean.Name → Lean.Name - updateName Mathlib.Tactic.Simps.Basic
Lean.Name → String → Bool → Lean.Name - Simps.projectionsInfo Mathlib.Tactic.Simps.Basic
List Simps.ProjectionData → String → Lean.Name → Lean.MessageData - Simps.getCompositeOfProjections Mathlib.Tactic.Simps.Basic
Lean.Name → String → Lean.MetaM (Lean.Expr × Array ℕ) - Simps.addProjections Mathlib.Tactic.Simps.Basic
Lean.Syntax → List Lean.Name → Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Array Lean.Expr → Bool → Simps.Config → List (String × Lean.Syntax) → List ℕ → Lean.MetaM (Array Lean.Name) - simpsTac Mathlib.Tactic.Simps.Basic
Lean.Syntax → Lean.Name → optParam Simps.Config { isSimp := true, attrs := [], simpRhs := false, typeMd := Lean.Meta.TransparencyMode.instances, rhsMd := Lean.Meta.TransparencyMode.reducible, fullyApplied := true, notRecursive := [`Prod, `PProd, `Opposite, `PreOpposite], debug := false } → optParam (List (String × Lean.Syntax)) [] → optParam Bool false → Lean.AttrM (Array Lean.Name) - ToAdditive.Config.mk Mathlib.Tactic.ToAdditive
Bool → Lean.Name → Option String → Bool → List (List ℕ) → Array Lean.Syntax → Lean.Syntax → Option Bool → ToAdditive.Config - ToAdditive.additivizeLemmas Mathlib.Tactic.ToAdditive
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadError m] → [inst : MonadLiftT Lean.CoreM m] → Array Lean.Name → String → (Lean.Name → m (Array Lean.Name)) → m Unit - ToAdditive.Config.mk.injEq Mathlib.Tactic.ToAdditive
∀ (trace : Bool) (tgt : Lean.Name) (doc : Option String) (allowAutoName : Bool) (reorder : List (List ℕ)) (attrs : Array Lean.Syntax) (ref : Lean.Syntax) (existing : Option Bool) (trace_1 : Bool) (tgt_1 : Lean.Name) (doc_1 : Option String) (allowAutoName_1 : Bool) (reorder_1 : List (List ℕ)) (attrs_1 : Array Lean.Syntax) (ref_1 : Lean.Syntax) (existing_1 : Option Bool), ({ trace := trace, tgt := tgt, doc := doc, allowAutoName := allowAutoName, reorder := reorder, attrs := attrs, ref := ref, existing := existing } = { trace := trace_1, tgt := tgt_1, doc := doc_1, allowAutoName := allowAutoName_1, reorder := reorder_1, attrs := attrs_1, ref := ref_1, existing := existing_1 }) = (trace = trace_1 ∧ tgt = tgt_1 ∧ doc = doc_1 ∧ allowAutoName = allowAutoName_1 ∧ reorder = reorder_1 ∧ attrs = attrs_1 ∧ ref = ref_1 ∧ existing = existing_1) - ToAdditive.Config.mk.sizeOf_spec Mathlib.Tactic.ToAdditive
∀ (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.mkModuleInitializationFunctionName Lean.Compiler.NameMangling
Lean.Name → String - Lean.Name.mangle Lean.Compiler.NameMangling
Lean.Name → optParam String "l_" → String - Lean.IR.EmitC.toCInitName Lean.Compiler.IR.EmitC
Lean.Name → Lean.IR.EmitC.M String - Lean.IR.EmitC.toCName Lean.Compiler.IR.EmitC
Lean.Name → Lean.IR.EmitC.M String - Lean.IR.emitC Lean.Compiler.IR.EmitC
Lean.Environment → Lean.Name → Except String String - Lean.IR.getCtorLayout Lean.Compiler.IR.CtorLayout
Lean.Environment → Lean.Name → Except String Lean.IR.CtorLayout - Lean.Compiler.LCNF.Testing.assertDoesNotContainConstAfter Lean.Compiler.LCNF.Testing
Lean.Name → String → Lean.Compiler.LCNF.Testing.TestInstaller - Lean.Elab.runFrontend Lean.Elab.Frontend
String → Lean.Options → String → Lean.Name → optParam UInt32 0 → optParam (Option String) none → optParam Bool false → IO (Lean.Environment × Bool) - Lean.Elab.sortDeclLevelParams Lean.Elab.DeclUtil
List Lean.Name → List Lean.Name → Array Lean.Name → Except String (List Lean.Name) - Lean.Elab.Command.NameGen.mkBaseNameWithSuffix' Lean.Elab.DeclNameGen
String → Array Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM Lean.Name - Lean.Elab.Term.Quotation.resolveSectionVariable Lean.Elab.Quotation
Lean.NameMap Lean.Name → Lean.Name → List (Lean.Name × List String) - Lean.Elab.Term.Quotation.resolveSectionVariable.loop Lean.Elab.Quotation
Lean.NameMap Lean.Name → Lean.MacroScopesView → Lean.Name → List String → List (Lean.Name × List String) - Lean.registerLabelAttr Lean.LabelAttribute
Lean.Name → String → autoParam Lean.Name _auto✝ → IO Lean.LabelExtension - Lean.mkLabelAttr Lean.LabelAttribute
Lean.Name → String → Lean.LabelExtension → autoParam Lean.Name _auto✝ → IO Unit - Lean.Meta.Rewrites.takeListAux Lean.Meta.Tactic.Rewrites
Lean.Meta.Rewrites.RewriteResultConfig → Lean.HashMap String Unit → Array Lean.Meta.Rewrites.RewriteResult → List ((Lean.Expr ⊕ Lean.Name) × Bool × ℕ) → Lean.MetaM (Array Lean.Meta.Rewrites.RewriteResult) - Lean.Elab.Deriving.mkContext Lean.Elab.Deriving.Util
String → Lean.Name → Lean.Elab.TermElabM Lean.Elab.Deriving.Context - Lean.ParseImports.moduleIdent.parse Lean.Elab.ParseImportsFast
Bool → String → Lean.Name → Lean.ParseImports.State → Lean.ParseImports.State - Aesop.registerTraceOption Aesop.Tracing
Lean.Name → String → IO Aesop.TraceOption - Aesop.LocalRuleSet.trace.printSimpSetName Aesop.RuleSet
Lean.Name → String - Lean.toModifiers Mathlib.Tactic.Core
Lean.Name → optParam (Option String) none → Lean.CoreM Lean.Elab.Modifiers - Lean.toPreDefinition Mathlib.Tactic.Core
Lean.Name → Lean.Name → Lean.Expr → Lean.Expr → optParam (Option String) none → Lean.CoreM Lean.Elab.PreDefinition - Std.CodeAction.holeKindToHoleString Batteries.CodeAction.Misc
Lean.Name → String → String - Lean.ParametricAttributeExtra.setParam Batteries.Lean.AttributeExtra
{α : Type} → Lean.ParametricAttributeExtra α → Lean.Environment → Lean.Name → α → Except String Lean.Environment - Lean.registerTagAttributeExtra Batteries.Lean.AttributeExtra
Lean.Name → String → List Lean.Name → (optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) → autoParam Lean.Name _auto✝ → IO Lean.TagAttributeExtra - Batteries.Tactic.DiscrTreeCache.mk Batteries.Util.Cache
{α : Type} → [inst : BEq α] → String → (Lean.Name → Lean.ConstantInfo → Lean.MetaM (Array (Array Lean.Meta.DiscrTree.Key × α))) → optParam (Option (Array α → Array α)) none → optParam (Lean.MetaM (Lean.Meta.DiscrTree α)) failure → IO (Batteries.Tactic.DiscrTreeCache α) - Batteries.Tactic.DeclCache.mk Batteries.Util.Cache
{α : Type} → String → optParam (Lean.MetaM α) failure → α → (addDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) → optParam (Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) addDecl → (optParam (α → Lean.MetaM α) fun a => pure a) → IO (Batteries.Tactic.DeclCache α) - Mathlib.Tactic.GCongr.mkForwardExt.unsafe_1 Mathlib.Tactic.GCongr.ForwardAttr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Tactic.GCongr.ForwardExt - Mathlib.Tactic.GCongr.mkForwardExt.unsafe_impl_1 Mathlib.Tactic.GCongr.ForwardAttr
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Tactic.GCongr.ForwardExt - Mathlib.Meta.NormNum.mkNormNumExt.unsafe_1 Mathlib.Tactic.NormNum.Core
Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Meta.NormNum.NormNumExt
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 c44d42e