Loogle!

Result

Found 3612 definitions mentioning Lean.Name. Of these, only the first 200 are shown.

• Lean.Name 📋 Init.Prelude
  : Type
• Lean.Name.anonymous 📋 Init.Prelude
  : Lean.Name
• Lean.extractMacroScopes 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroScopesView
• Lean.instAppendName 📋 Init.Prelude
  : Append Lean.Name
• Lean.instHashableName 📋 Init.Prelude
  : Hashable Lean.Name
• Lean.instInhabitedName 📋 Init.Prelude
  : Inhabited Lean.Name
• Lean.Macro.getCurrNamespace 📋 Init.Prelude
  : Lean.MacroM Lean.Name
• Lean.MacroScopesView.imported 📋 Init.Prelude
  (self : Lean.MacroScopesView) : Lean.Name
• Lean.MacroScopesView.mainModule 📋 Init.Prelude
  (self : Lean.MacroScopesView) : Lean.Name
• Lean.MacroScopesView.name 📋 Init.Prelude
  (self : Lean.MacroScopesView) : Lean.Name
• Lean.MacroScopesView.review 📋 Init.Prelude
  (view : Lean.MacroScopesView) : Lean.Name
• Lean.Name.eraseMacroScopes 📋 Init.Prelude
  (n : Lean.Name) : Lean.Name
• Lean.Name.hasMacroScopes 📋 Init.Prelude
  : Lean.Name → Bool
• Lean.Name.hash 📋 Init.Prelude
  : Lean.Name → UInt64
• Lean.Name.instBEq 📋 Init.Prelude
  : BEq Lean.Name
• Lean.Name.mkSimple 📋 Init.Prelude
  (s : String) : Lean.Name
• Lean.Name.mkStr1 📋 Init.Prelude
  (s₁ : String) : Lean.Name
• Lean.Name.simpMacroScopes 📋 Init.Prelude
  (n : Lean.Name) : Lean.Name
• Lean.ParserDescr.const 📋 Init.Prelude
  (name : Lean.Name) : Lean.ParserDescr
• Lean.ParserDescr.parser 📋 Init.Prelude
  (declName : Lean.Name) : Lean.ParserDescr
• Lean.Syntax.getId 📋 Init.Prelude
  : Lean.Syntax → Lean.Name
• Lean.Macro.Context.mainModule 📋 Init.Prelude
  (self : Lean.Macro.Context) : Lean.Name
• Lean.Syntax.Preresolved.namespace 📋 Init.Prelude
  (ns : Lean.Name) : Lean.Syntax.Preresolved
• Lean.Macro.addMacroScope 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM Lean.Name
• Lean.Macro.hasDecl 📋 Init.Prelude
  (declName : Lean.Name) : Lean.MacroM Bool
• Lean.Name.append 📋 Init.Prelude
  (a b : Lean.Name) : Lean.Name
• Lean.Name.appendCore 📋 Init.Prelude
  : Lean.Name → Lean.Name → Lean.Name
• Lean.Name.mkNum 📋 Init.Prelude
  (p : Lean.Name) (v : ℕ) : 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.num 📋 Init.Prelude
  (pre : Lean.Name) (i : ℕ) : Lean.Name
• Lean.Name.str 📋 Init.Prelude
  (pre : Lean.Name) (str : String) : Lean.Name
• Lean.ParserDescr.cat 📋 Init.Prelude
  (catName : Lean.Name) (rbp : ℕ) : Lean.ParserDescr
• Lean.ParserDescr.unary 📋 Init.Prelude
  (name : Lean.Name) (p : Lean.ParserDescr) : Lean.ParserDescr
• Lean.Syntax.matchesIdent 📋 Init.Prelude
  (stx : Lean.Syntax) (id : Lean.Name) : Bool
• Lean.Macro.Methods.getCurrNamespace 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.MacroM Lean.Name
• Lean.addMacroScope 📋 Init.Prelude
  (mainModule n : Lean.Name) (scp : Lean.MacroScope) : Lean.Name
• Lean.Macro.resolveNamespace 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM (List Lean.Name)
• Lean.Macro.trace 📋 Init.Prelude
  (clsName : Lean.Name) (msg : String) : Lean.MacroM Unit
• Lean.Name.beq 📋 Init.Prelude
  : Lean.Name → Lean.Name → Bool
• Lean.Name.mkStr3 📋 Init.Prelude
  (s₁ s₂ s₃ : String) : Lean.Name
• Lean.ParserDescr.binary 📋 Init.Prelude
  (name : Lean.Name) (p₁ p₂ : Lean.ParserDescr) : Lean.ParserDescr
• Lean.Macro.Methods.hasDecl 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.Name → Lean.MacroM Bool
• 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.Methods.resolveNamespace 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.Name → Lean.MacroM (List Lean.Name)
• Lean.Macro.State.traceMsgs 📋 Init.Prelude
  (self : Lean.Macro.State) : List (Lean.Name × String)
• Lean.MacroScopesView.mk 📋 Init.Prelude
  (name imported mainModule : Lean.Name) (scopes : List Lean.MacroScope) : Lean.MacroScopesView
• Lean.MonadQuotation.getMainModule 📋 Init.Prelude
  {m : Type → Type} [self : Lean.MonadQuotation m] : m Lean.Name
• Lean.Name.mkStr5 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ : String) : Lean.Name
• Lean.Syntax.ident 📋 Init.Prelude
  (info : Lean.SourceInfo) (rawVal : Substring) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) : Lean.Syntax
• 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.Macro.Context.mk 📋 Init.Prelude
  (methods : Lean.Macro.MethodsRef✝) (mainModule : Lean.Name) (currMacroScope : Lean.MacroScope) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) : Lean.Macro.Context
• 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.MonadQuotation.addMacroScope 📋 Init.Prelude
  {m : Type → Type} [Lean.MonadQuotation m] [Monad m] (n : Lean.Name) : m Lean.Name
• Lean.Name.mkStr8 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Lean.Name
• Lean.MonadQuotation.mk 📋 Init.Prelude
  {m : Type → Type} [toMonadRef : Lean.MonadRef m] (getCurrMacroScope : m Lean.MacroScope) (getMainModule : m Lean.Name) (withFreshMacroScope : {α : Type} → m α → m α) : Lean.MonadQuotation m
• 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.instSizeOfName 📋 Init.SizeOf
  : SizeOf Lean.Name
• Lean.Name.sizeOf 📋 Init.SizeOf
  : Lean.Name → ℕ
• Lean.Name.anonymous.sizeOf_spec 📋 Init.SizeOf
  : sizeOf Lean.Name.anonymous = 1
• Lean.ParserDescr.const.sizeOf_spec 📋 Init.SizeOf
  (name : Lean.Name) : sizeOf (Lean.ParserDescr.const name) = 1 + sizeOf name
• Lean.ParserDescr.parser.sizeOf_spec 📋 Init.SizeOf
  (declName : Lean.Name) : sizeOf (Lean.ParserDescr.parser declName) = 1 + sizeOf declName
• 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.num.sizeOf_spec 📋 Init.SizeOf
  (p : Lean.Name) (n : ℕ) : sizeOf (p.num n) = 1 + sizeOf p + sizeOf n
• Lean.Name.str.sizeOf_spec 📋 Init.SizeOf
  (p : Lean.Name) (s : String) : sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
• Lean.ParserDescr.cat.sizeOf_spec 📋 Init.SizeOf
  (catName : Lean.Name) (rbp : ℕ) : sizeOf (Lean.ParserDescr.cat catName rbp) = 1 + sizeOf catName + sizeOf rbp
• Lean.ParserDescr.unary.sizeOf_spec 📋 Init.SizeOf
  (name : Lean.Name) (p : Lean.ParserDescr) : sizeOf (Lean.ParserDescr.unary name p) = 1 + sizeOf name + sizeOf p
• Lean.ParserDescr.binary.sizeOf_spec 📋 Init.SizeOf
  (name : Lean.Name) (p₁ p₂ : Lean.ParserDescr) : sizeOf (Lean.ParserDescr.binary name p₁ p₂) = 1 + sizeOf name + sizeOf p₁ + sizeOf p₂
• 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.MacroScopesView.mk.sizeOf_spec 📋 Init.SizeOf
  (name imported mainModule : Lean.Name) (scopes : List Lean.MacroScope) : sizeOf { name := name, imported := imported, mainModule := mainModule, scopes := scopes } = 1 + sizeOf name + sizeOf imported + sizeOf mainModule + sizeOf scopes
• Lean.Syntax.ident.sizeOf_spec 📋 Init.SizeOf
  (info : Lean.SourceInfo) (rawVal : Substring) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) : sizeOf (Lean.Syntax.ident info rawVal val preresolved) = 1 + sizeOf info + sizeOf rawVal + sizeOf val + sizeOf preresolved
• Lean.Macro.Context.mk.sizeOf_spec 📋 Init.SizeOf
  (methods : Lean.Macro.MethodsRef✝) (mainModule : Lean.Name) (currMacroScope : Lean.MacroScope) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) : sizeOf { methods := methods, mainModule := mainModule, currMacroScope := currMacroScope, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth, ref := ref } = 1 + sizeOf methods + sizeOf mainModule + sizeOf currMacroScope + sizeOf currRecDepth + sizeOf maxRecDepth + sizeOf ref
• Lean.Name.num.injEq 📋 Init.Core
  (pre : Lean.Name) (i : ℕ) (pre✝ : Lean.Name) (i✝ : ℕ) : (pre.num i = pre✝.num i✝) = (pre = pre✝ ∧ i = i✝)
• 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✝)
• Lean.Syntax.ident.injEq 📋 Init.Core
  (info : Lean.SourceInfo) (rawVal : Substring) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) (info✝ : Lean.SourceInfo) (rawVal✝ : Substring) (val✝ : Lean.Name) (preresolved✝ : List Lean.Syntax.Preresolved) : (Lean.Syntax.ident info rawVal val preresolved = Lean.Syntax.ident info✝ rawVal✝ val✝ preresolved✝) = (info = info✝ ∧ rawVal = rawVal✝ ∧ val = val✝ ∧ preresolved = preresolved✝)
• Lean.NameGenerator.namePrefix 📋 Init.MetaTypes
  (self : Lean.NameGenerator) : Lean.Name
• Lean.NameGenerator.mk 📋 Init.MetaTypes
  (namePrefix : Lean.Name) (idx : ℕ) : Lean.NameGenerator
• Lean.NameGenerator.mk.injEq 📋 Init.MetaTypes
  (namePrefix : Lean.Name) (idx : ℕ) (namePrefix✝ : Lean.Name) (idx✝ : ℕ) : ({ namePrefix := namePrefix, idx := idx } = { namePrefix := namePrefix✝, idx := idx✝ }) = (namePrefix = namePrefix✝ ∧ idx = idx✝)
• Lean.NameGenerator.mk.sizeOf_spec 📋 Init.MetaTypes
  (namePrefix : Lean.Name) (idx : ℕ) : sizeOf { namePrefix := namePrefix, idx := idx } = 1 + sizeOf namePrefix + sizeOf idx
• Lean.mkCIdent 📋 Init.Meta
  (c : Lean.Name) : Lean.Ident
• Lean.mkIdent 📋 Init.Meta
  (val : Lean.Name) : Lean.Ident
• Lean.quoteNameMk 📋 Init.Meta
  : Lean.Name → Lean.Term
• String.toName 📋 Init.Meta
  (s : String) : Lean.Name
• Substring.toName 📋 Init.Meta
  (s : Substring) : Lean.Name
• Lean.Name.capitalize 📋 Init.Meta
  : Lean.Name → Lean.Name
• Lean.Name.getRoot 📋 Init.Meta
  : Lean.Name → Lean.Name
• Lean.Name.instDecidableEq 📋 Init.Meta
  : DecidableEq Lean.Name
• Lean.Name.instRepr 📋 Init.Meta
  : Repr Lean.Name
• Lean.Name.instToString 📋 Init.Meta
  : ToString Lean.Name
• Lean.Name.isInaccessibleUserName 📋 Init.Meta
  : Lean.Name → Bool
• Lean.NameGenerator.curr 📋 Init.Meta
  (g : Lean.NameGenerator) : Lean.Name
• Lean.TSyntax.getHygieneInfo 📋 Init.Meta
  (s : Lean.HygieneInfo) : Lean.Name
• Lean.TSyntax.getId 📋 Init.Meta
  (s : Lean.Ident) : Lean.Name
• Lean.TSyntax.getName 📋 Init.Meta
  (s : Lean.NameLit) : Lean.Name
• Lean.Name.toString.maybePseudoSyntax 📋 Init.Meta
  (n : Lean.Name) : Bool
• 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.Name.appendIndexAfter 📋 Init.Meta
  (n : Lean.Name) (idx : ℕ) : Lean.Name
• Lean.Name.instLawfulBEq 📋 Init.Meta
  : LawfulBEq Lean.Name
• Lean.Name.reprPrec 📋 Init.Meta
  (n : Lean.Name) (prec : ℕ) : Lean.Format
• Lean.Syntax.decodeNameLit 📋 Init.Meta
  (s : String) : Option Lean.Name
• Lean.Syntax.getOptionalIdent? 📋 Init.Meta
  (stx : Lean.Syntax) : Option Lean.Name
• Lean.Syntax.isNameLit? 📋 Init.Meta
  (stx : Lean.Syntax) : Option Lean.Name
• Lean.instQuoteNameMkStr1 📋 Init.Meta
  : Lean.Quote Lean.Name
• Lean.Name.eraseSuffix? 📋 Init.Meta
  : Lean.Name → Lean.Name → Option Lean.Name
• Lean.Name.modifyBase 📋 Init.Meta
  (n : Lean.Name) (f : Lean.Name → Lean.Name) : Lean.Name
• Lean.Name.replacePrefix 📋 Init.Meta
  : Lean.Name → Lean.Name → Lean.Name → Lean.Name
• Lean.mkCIdentFrom 📋 Init.Meta
  (src : Lean.Syntax) (c : Lean.Name) (canonical : Bool := false) : Lean.Ident
• Lean.mkIdentFrom 📋 Init.Meta
  (src : Lean.Syntax) (val : Lean.Name) (canonical : Bool := false) : Lean.Ident
• Lean.HygieneInfo.mkIdent 📋 Init.Meta
  (s : Lean.HygieneInfo) (val : Lean.Name) (canonical : Bool := false) : Lean.Ident
• Lean.mkFreshId 📋 Init.Meta
  {m : Type → Type} [Monad m] [Lean.MonadNameGenerator m] : m Lean.Name
• Lean.Name.toStringWithSep 📋 Init.Meta
  (sep : String) (escape : Bool) (n : Lean.Name) (isToken : String → Bool := fun x => false) : String
• Lean.Syntax.mkCApp 📋 Init.Meta
  (fn : Lean.Name) (args : Lean.TSyntaxArray `term) : Lean.Term
• Lean.Name.toString 📋 Init.Meta
  (n : Lean.Name) (escape : Bool := true) (isToken : String → Bool := fun x => false) : String
• Lean.mkCIdentFromRef 📋 Init.Meta
  {m : Type → Type} [Monad m] [Lean.MonadRef m] (c : Lean.Name) (canonical : Bool := false) : m Lean.Syntax
• Lean.mkIdentFromRef 📋 Init.Meta
  {m : Type → Type} [Monad m] [Lean.MonadRef m] (val : Lean.Name) (canonical : Bool := false) : m Lean.Ident
• Lean.Name.beq_iff_eq 📋 Init.Meta
  {m n : Lean.Name} : (m == n) = true ↔ m = n
• Lean.TSyntax.instCoeDepTermMkIdentIdent 📋 Init.Meta
  {info : Lean.SourceInfo} {ss : Substring} {n : Lean.Name} {res : List Lean.Syntax.Preresolved} : CoeDep Lean.Term { raw := Lean.Syntax.ident info ss n res } Lean.Ident
• 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_3 📋 Init.Meta
  (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ) : (p₁.num n₁).beq (p₂.num n₂) = (n₁ == n₂ && p₁.beq p₂)
• Lean.Name.beq.eq_4 📋 Init.Meta
  (x✝ x✝¹ : Lean.Name) (x_4 : x✝ = Lean.Name.anonymous → x✝¹ = Lean.Name.anonymous → False) (x_5 : ∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), x✝ = p₁.str s₁ → x✝¹ = p₂.str s₂ → False) (x_6 : ∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), x✝ = p₁.num n₁ → x✝¹ = p₂.num n₂ → False) : x✝.beq x✝¹ = false
• Lean.expandBrackedBinders 📋 Init.NotationExtra
  (combinatorDeclName : Lean.Name) (bracketedExplicitBinders body : Lean.Syntax) : Lean.MacroM Lean.Syntax
• Lean.expandExplicitBinders 📋 Init.NotationExtra
  (combinatorDeclName : Lean.Name) (explicitBinders body : Lean.Syntax) : Lean.MacroM Lean.Syntax
• Dynamic.typeName 📋 Init.Dynamic
  (any : Dynamic) : Lean.Name
• TypeName.mk 📋 Init.Dynamic
  (α : Type u) (typeName : Lean.Name) : TypeName α
• TypeName.typeName 📋 Init.Dynamic
  (α : Type u_1) [TypeName α] : Lean.Name
• Lean.DataValue.ofName 📋 Lean.Data.KVMap
  (v : Lean.Name) : Lean.DataValue
• Lean.KVMap.instValueName 📋 Lean.Data.KVMap
  : Lean.KVMap.Value Lean.Name
• Lean.instCoeNameDataValue 📋 Lean.Data.KVMap
  : Coe Lean.Name Lean.DataValue
• Lean.KVMap.contains 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (n : Lean.Name) : Bool
• Lean.KVMap.erase 📋 Lean.Data.KVMap
  : Lean.KVMap → Lean.Name → Lean.KVMap
• Lean.KVMap.find 📋 Lean.Data.KVMap
  : Lean.KVMap → Lean.Name → Option Lean.DataValue
• Lean.KVMap.findD 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (d₀ : Lean.DataValue) : Lean.DataValue
• Lean.KVMap.insert 📋 Lean.Data.KVMap
  : Lean.KVMap → Lean.Name → Lean.DataValue → Lean.KVMap
• Lean.KVMap.setBool 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (v : Bool) : Lean.KVMap
• Lean.KVMap.setInt 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (v : ℤ) : Lean.KVMap
• Lean.KVMap.setName 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k v : Lean.Name) : Lean.KVMap
• Lean.KVMap.setNat 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (v : ℕ) : Lean.KVMap
• Lean.KVMap.setString 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (v : String) : Lean.KVMap
• Lean.KVMap.setSyntax 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (v : Lean.Syntax) : Lean.KVMap
• Lean.KVMap.entries 📋 Lean.Data.KVMap
  (self : Lean.KVMap) : List (Lean.Name × Lean.DataValue)
• Lean.KVMap.mk 📋 Lean.Data.KVMap
  (entries : List (Lean.Name × Lean.DataValue)) : Lean.KVMap
• Lean.KVMap.updateBool 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : Bool → Bool) : Lean.KVMap
• Lean.KVMap.updateInt 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : ℤ → ℤ) : Lean.KVMap
• Lean.KVMap.updateName 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : Lean.Name → Lean.Name) : Lean.KVMap
• Lean.KVMap.updateNat 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : ℕ → ℕ) : Lean.KVMap
• Lean.KVMap.updateString 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : String → String) : Lean.KVMap
• Lean.KVMap.updateSyntax 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : Lean.Syntax → Lean.Syntax) : Lean.KVMap
• Lean.KVMap.getBool 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : Bool := false) : Bool
• Lean.KVMap.getName 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : Lean.Name := Lean.Name.anonymous) : Lean.Name
• Lean.KVMap.getString 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : String := "") : String
• Lean.KVMap.getSyntax 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : Lean.Syntax := Lean.Syntax.missing) : Lean.Syntax
• Lean.KVMap.subsetAux 📋 Lean.Data.KVMap
  : List (Lean.Name × Lean.DataValue) → Lean.KVMap → Bool
• Lean.KVMap.findCore 📋 Lean.Data.KVMap
  : List (Lean.Name × Lean.DataValue) → Lean.Name → Option Lean.DataValue
• Lean.KVMap.get 📋 Lean.Data.KVMap
  {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (defVal : α) : α
• Lean.KVMap.get? 📋 Lean.Data.KVMap
  {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) : Option α
• Lean.KVMap.mergeBy 📋 Lean.Data.KVMap
  (mergeFn : Lean.Name → Lean.DataValue → Lean.DataValue → Lean.DataValue) (l r : Lean.KVMap) : Lean.KVMap
• Lean.KVMap.set 📋 Lean.Data.KVMap
  {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (v : α) : Lean.KVMap
• Lean.KVMap.instForInProdNameDataValue 📋 Lean.Data.KVMap
  {m : Type u_1 → Type u_2} : ForIn m Lean.KVMap (Lean.Name × Lean.DataValue)
• Lean.KVMap.getInt 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : ℤ := 0) : ℤ
• Lean.KVMap.getNat 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : ℕ := 0) : ℕ
• Lean.KVMap.insertCore 📋 Lean.Data.KVMap
  : List (Lean.Name × Lean.DataValue) → Lean.Name → Lean.DataValue → List (Lean.Name × Lean.DataValue)
• Lean.KVMap.update 📋 Lean.Data.KVMap
  {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (f : Option α → Option α) : Lean.KVMap
• Lean.DataValue.ofName.injEq 📋 Lean.Data.KVMap
  (v v✝ : Lean.Name) : (Lean.DataValue.ofName v = Lean.DataValue.ofName v✝) = (v = v✝)
• Lean.KVMap.forIn 📋 Lean.Data.KVMap
  {δ : Type w} {m : Type w → Type w'} [Monad m] (kv : Lean.KVMap) (init : δ) (f : Lean.Name × Lean.DataValue → δ → m (ForInStep δ)) : m δ
• Lean.KVMap.mk.injEq 📋 Lean.Data.KVMap
  (entries entries✝ : List (Lean.Name × Lean.DataValue)) : ({ entries := entries } = { entries := entries✝ }) = (entries = entries✝)
• Lean.DataValue.ofName.sizeOf_spec 📋 Lean.Data.KVMap
  (v : Lean.Name) : sizeOf (Lean.DataValue.ofName v) = 1 + sizeOf v
• Lean.KVMap.mk.sizeOf_spec 📋 Lean.Data.KVMap
  (entries : List (Lean.Name × Lean.DataValue)) : sizeOf { entries := entries } = 1 + sizeOf entries
• Lean.Name.getNumParts 📋 Lean.Data.Name
  : Lean.Name → ℕ
• Lean.Name.getPrefix 📋 Lean.Data.Name
  : Lean.Name → Lean.Name
• Lean.Name.getString! 📋 Lean.Data.Name
  : Lean.Name → String
• Lean.Name.hasNum 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.hashEx 📋 Lean.Data.Name
  : Lean.Name → UInt64
• Lean.Name.isAnonymous 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isAtomic 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isImplementationDetail 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isInternal 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isInternalDetail 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isInternalOrNum 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isNum 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.isStr 📋 Lean.Data.Name
  : Lean.Name → Bool
• Lean.Name.cmp 📋 Lean.Data.Name
  : Lean.Name → Lean.Name → Ordering
• Lean.Name.components 📋 Lean.Data.Name
  (n : Lean.Name) : List Lean.Name
• Lean.Name.componentsRev 📋 Lean.Data.Name
  : Lean.Name → List Lean.Name
• Lean.Name.eqStr 📋 Lean.Data.Name
  : Lean.Name → String → Bool
• Lean.Name.isPrefixOf 📋 Lean.Data.Name
  : Lean.Name → Lean.Name → Bool
• Lean.Name.isSuffixOf 📋 Lean.Data.Name
  : Lean.Name → Lean.Name → Bool
• Lean.Name.lt 📋 Lean.Data.Name
  (x y : Lean.Name) : Bool
• Lean.Name.quickCmp 📋 Lean.Data.Name
  (n₁ n₂ : Lean.Name) : Ordering
• Lean.Name.quickCmpAux 📋 Lean.Data.Name
  : Lean.Name → Lean.Name → Ordering
• Lean.Name.quickLt 📋 Lean.Data.Name
  (n₁ n₂ : Lean.Name) : Bool
• Lean.Name.updatePrefix 📋 Lean.Data.Name
  : Lean.Name → Lean.Name → Lean.Name
• Lean.Name.anyS 📋 Lean.Data.Name
  (n : Lean.Name) (f : String → Bool) : Bool
• Lean.NameHashSet.contains 📋 Lean.Data.NameMap
  (s : Lean.NameHashSet) (n : Lean.Name) : Bool
• Lean.NameSSet.contains 📋 Lean.Data.NameMap
  (s : Lean.NameSSet) (n : Lean.Name) : Bool
• Lean.NameSSet.insert 📋 Lean.Data.NameMap
  (s : Lean.NameSSet) (n : Lean.Name) : Lean.NameSSet

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, _ * _, _ ^ _, |- _ < _ → _
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 provided by the Lean FRO.

This is Loogle revision 026c9d9 serving mathlib revision 0e2973b