Loogle!

Result

Found 1265 definitions whose name contains "Name". Of these, only the first 200 are shown.

• Lean.Name 📋 Init.Prelude
  : Type
• Lean.nameLitKind 📋 Init.Prelude
  : Lean.SyntaxNodeKind
• Lean.Name.anonymous 📋 Init.Prelude
  : Lean.Name
• 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.name 📋 Init.Prelude
  (self : 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.Syntax.Preresolved.namespace 📋 Init.Prelude
  (ns : Lean.Name) : Lean.Syntax.Preresolved
• 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.Macro.Methods.getCurrNamespace 📋 Init.Prelude
  (self : Lean.Macro.Methods) : Lean.MacroM Lean.Name
• Lean.Macro.resolveNamespace 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM (List Lean.Name)
• Lean.Name.beq 📋 Init.Prelude
  : Lean.Name → Lean.Name → Bool
• Lean.Name.mkStr3 📋 Init.Prelude
  (s₁ s₂ s₃ : String) : Lean.Name
• 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.Name.mkStr5 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ : String) : Lean.Name
• Lean.Macro.resolveGlobalName 📋 Init.Prelude
  (n : Lean.Name) : Lean.MacroM (List (Lean.Name × List String))
• Lean.Name.mkStr6 📋 Init.Prelude
  (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Lean.Name
• namedPattern 📋 Init.Prelude
  {α : Sort u} (x a : α) (h : x = a) : α
• 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.Parser.Tactic.rename 📋 Init.Tactics
  : Lean.ParserDescr
• Lean.Parser.Tactic.renameI 📋 Init.Tactics
  : Lean.ParserDescr
• 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.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.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.NameGenerator 📋 Init.MetaTypes
  : Type
• Lean.instInhabitedNameGenerator 📋 Init.MetaTypes
  : Inhabited Lean.NameGenerator
• Lean.NameGenerator.idx 📋 Init.MetaTypes
  (self : Lean.NameGenerator) : ℕ
• 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.Syntax.NameLit 📋 Init.Meta
  : Type
• 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.NameGenerator.next 📋 Init.Meta
  (g : Lean.NameGenerator) : Lean.NameGenerator
• Lean.TSyntax.getName 📋 Init.Meta
  (s : Lean.NameLit) : Lean.Name
• Lean.Name.toString.maybePseudoSyntax 📋 Init.Meta
  (n : Lean.Name) : Bool
• Lean.MonadNameGenerator 📋 Init.Meta
  (m : Type → Type) : Type
• 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.isNameLit? 📋 Init.Meta
  (stx : Lean.Syntax) : Option Lean.Name
• Lean.Syntax.splitNameLit 📋 Init.Meta
  (ss : Substring) : List Substring
• Lean.TSyntax.instCoeNameLitTerm 📋 Init.Meta
  : Coe Lean.NameLit Lean.Term
• 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.NameGenerator.mkChild 📋 Init.Meta
  (g : Lean.NameGenerator) : Lean.NameGenerator × Lean.NameGenerator
• Lean.Name.toStringWithSep.maybeEscape 📋 Init.Meta
  (escape : Bool) (s : String) (force : Bool) : String
• Lean.Syntax.mkNameLit 📋 Init.Meta
  (val : String) (info : Lean.SourceInfo := Lean.SourceInfo.none) : Lean.NameLit
• Lean.MonadNameGenerator.getNGen 📋 Init.Meta
  {m : Type → Type} [self : Lean.MonadNameGenerator m] : m Lean.NameGenerator
• Lean.Name.escapePart 📋 Init.Meta
  (s : String) (force : Bool := false) : Option String
• Lean.Name.beq.eq_1 📋 Init.Meta
  : Lean.Name.anonymous.beq Lean.Name.anonymous = true
• Lean.MonadNameGenerator.setNGen 📋 Init.Meta
  {m : Type → Type} [self : Lean.MonadNameGenerator m] : Lean.NameGenerator → m Unit
• Lean.MonadNameGenerator.mk 📋 Init.Meta
  {m : Type → Type} (getNGen : m Lean.NameGenerator) (setNGen : Lean.NameGenerator → m Unit) : Lean.MonadNameGenerator m
• 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.monadNameGeneratorLift 📋 Init.Meta
  (m n : Type → Type) [MonadLift m n] [Lean.MonadNameGenerator m] : Lean.MonadNameGenerator n
• Lean.Name.beq_iff_eq 📋 Init.Meta
  {m n : Lean.Name} : (m == n) = true ↔ m = n
• 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
• System.FilePath.fileName 📋 Init.System.FilePath
  (p : System.FilePath) : Option String
• System.FilePath.withFileName 📋 Init.System.FilePath
  (p : System.FilePath) (fname : String) : System.FilePath
• IO.FS.DirEntry.fileName 📋 Init.System.IO
  (self : IO.FS.DirEntry) : String
• IO.FS.rename 📋 Init.System.IO
  (old new : System.FilePath) : IO Unit
• TypeName 📋 Init.Dynamic
  (α : Type u) : Type
• Dynamic.typeName 📋 Init.Dynamic
  (any : Dynamic) : Lean.Name
• instNonemptyTypeName 📋 Init.Dynamic
  {α : Type u_1} : Nonempty (TypeName α)
• 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.setName 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k v : Lean.Name) : Lean.KVMap
• Lean.KVMap.updateName 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (f : Lean.Name → Lean.Name) : Lean.KVMap
• Lean.KVMap.getName 📋 Lean.Data.KVMap
  (m : Lean.KVMap) (k : Lean.Name) (defVal : Lean.Name := Lean.Name.anonymous) : Lean.Name
• Lean.KVMap.instForInProdNameDataValue 📋 Lean.Data.KVMap
  {m : Type u_1 → Type u_2} : ForIn m Lean.KVMap (Lean.Name × Lean.DataValue)
• Lean.DataValue.ofName.injEq 📋 Lean.Data.KVMap
  (v v✝ : Lean.Name) : (Lean.DataValue.ofName v = Lean.DataValue.ofName v✝) = (v = v✝)
• Lean.DataValue.ofName.sizeOf_spec 📋 Lean.Data.KVMap
  (v : Lean.Name) : sizeOf (Lean.DataValue.ofName v) = 1 + sizeOf v
• 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.isInternalDetail.matchPrefix 📋 Lean.Data.Name
  (s pre : String) : Bool
• Lean.Name.anyS 📋 Lean.Data.Name
  (n : Lean.Name) (f : String → Bool) : Bool
• Lean.NameHashSet 📋 Lean.Data.NameMap
  : Type
• Lean.NameSSet 📋 Lean.Data.NameMap
  : Type
• Lean.NameSet 📋 Lean.Data.NameMap
  : Type
• Lean.NameHashSet.empty 📋 Lean.Data.NameMap
  : Lean.NameHashSet
• Lean.NameSSet.empty 📋 Lean.Data.NameMap
  : Lean.NameSSet
• Lean.NameSet.empty 📋 Lean.Data.NameMap
  : Lean.NameSet
• Lean.NameMap 📋 Lean.Data.NameMap
  (α : Type) : Type
• Lean.NameHashSet.instEmptyCollection 📋 Lean.Data.NameMap
  : EmptyCollection Lean.NameHashSet
• Lean.NameHashSet.instInhabited 📋 Lean.Data.NameMap
  : Inhabited Lean.NameHashSet
• Lean.NameSSet.instEmptyCollection 📋 Lean.Data.NameMap
  : EmptyCollection Lean.NameSSet
• Lean.NameSSet.instInhabited 📋 Lean.Data.NameMap
  : Inhabited Lean.NameSSet
• Lean.NameSet.instAppend 📋 Lean.Data.NameMap
  : Append Lean.NameSet
• Lean.NameSet.instEmptyCollection 📋 Lean.Data.NameMap
  : EmptyCollection Lean.NameSet
• Lean.NameSet.instInhabited 📋 Lean.Data.NameMap
  : Inhabited Lean.NameSet
• Lean.mkNameMap 📋 Lean.Data.NameMap
  (α : Type) : Lean.NameMap α
• 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
• Lean.NameSet.append 📋 Lean.Data.NameMap
  (s t : Lean.NameSet) : Lean.NameSet
• Lean.NameSet.contains 📋 Lean.Data.NameMap
  (s : Lean.NameSet) (n : Lean.Name) : Bool
• Lean.NameSet.insert 📋 Lean.Data.NameMap
  (s : Lean.NameSet) (n : Lean.Name) : Lean.NameSet
• Lean.NameHashSet.filter 📋 Lean.Data.NameMap
  (f : Lean.Name → Bool) (s : Lean.NameHashSet) : Lean.NameHashSet
• Lean.NameMap.instEmptyCollection 📋 Lean.Data.NameMap
  (α : Type) : EmptyCollection (Lean.NameMap α)
• Lean.NameMap.instInhabited 📋 Lean.Data.NameMap
  (α : Type) : Inhabited (Lean.NameMap α)
• Lean.NameSet.filter 📋 Lean.Data.NameMap
  (f : Lean.Name → Bool) (s : Lean.NameSet) : Lean.NameSet
• Lean.NameMap.contains 📋 Lean.Data.NameMap
  {α : Type} (m : Lean.NameMap α) (n : Lean.Name) : Bool
• Lean.NameHashSet.insert 📋 Lean.Data.NameMap
  (s : Lean.NameHashSet) (n : Lean.Name) : Std.HashSet Lean.Name
• Lean.NameMap.find? 📋 Lean.Data.NameMap
  {α : Type} (m : Lean.NameMap α) (n : Lean.Name) : Option α
• Lean.NameSet.instForInName 📋 Lean.Data.NameMap
  {m : Type u_1 → Type u_2} : ForIn m Lean.NameSet Lean.Name
• Lean.NameMap.filter 📋 Lean.Data.NameMap
  {α : Type} (f : Lean.Name → α → Bool) (m : Lean.NameMap α) : Lean.NameMap α
• Lean.NameMap.insert 📋 Lean.Data.NameMap
  {α : Type} (m : Lean.NameMap α) (n : Lean.Name) (a : α) : Lean.RBMap Lean.Name α Lean.Name.quickCmp
• Lean.NameMap.filterMap 📋 Lean.Data.NameMap
  {α β : Type} (f : Lean.Name → α → Option β) (m : Lean.NameMap α) : Lean.NameMap β
• Lean.NameMap.instForInProdName 📋 Lean.Data.NameMap
  {α : Type} {m : Type u_1 → Type u_2} : ForIn m (Lean.NameMap α) (Lean.Name × α)
• Lean.OptionDecl.declName 📋 Lean.Data.Options
  (self : Lean.OptionDecl) : Lean.Name
• Lean.Option.name 📋 Lean.Data.Options
  {α : Type} (self : Lean.Option α) : Lean.Name
• Lean.instForInOptionsProdNameDataValue 📋 Lean.Data.Options
  {m : Type u_1 → Type u_2} : ForIn m Lean.Options (Lean.Name × Lean.DataValue)
• Lean.getPPFullNames 📋 Lean.PrettyPrinter.Delaborator.Options
  (o : Lean.Options) : Bool
• Lean.getPPPrivateNames 📋 Lean.PrettyPrinter.Delaborator.Options
  (o : Lean.Options) : Bool
• Lean.pp.fullNames 📋 Lean.PrettyPrinter.Delaborator.Options
  : Lean.Option Bool
• Lean.pp.privateNames 📋 Lean.PrettyPrinter.Delaborator.Options
  : Lean.Option Bool
• Lean.instToFormatName_lean 📋 Lean.Data.Format
  : Lean.ToFormat Lean.Name
• Lean.instToFormatProdNameDataValue 📋 Lean.Data.Format
  : Lean.ToFormat (Lean.Name × Lean.DataValue)
• Lean.NameSanitizerState 📋 Lean.Hygiene
  : Type
• Lean.getSanitizeNames 📋 Lean.Hygiene
  (o : Lean.Options) : Bool
• Lean.NameSanitizerState.options 📋 Lean.Hygiene
  (self : Lean.NameSanitizerState) : Lean.Options
• Lean.pp.sanitizeNames 📋 Lean.Hygiene
  : Lean.Option Bool
• Lean.NameSanitizerState.nameStem2Idx 📋 Lean.Hygiene
  (self : Lean.NameSanitizerState) : Lean.NameMap ℕ
• Lean.NameSanitizerState.userName2Sanitized 📋 Lean.Hygiene
  (self : Lean.NameSanitizerState) : Lean.NameMap Lean.Name
• Lean.sanitizeName 📋 Lean.Hygiene
  (userName : Lean.Name) : StateM Lean.NameSanitizerState Lean.Name
• Lean.NameSanitizerState.mk 📋 Lean.Hygiene
  (options : Lean.Options) (nameStem2Idx : Lean.NameMap ℕ) (userName2Sanitized : Lean.NameMap Lean.Name) : Lean.NameSanitizerState
• Lean.NameSanitizerState.mk.injEq 📋 Lean.Hygiene
  (options : Lean.Options) (nameStem2Idx : Lean.NameMap ℕ) (userName2Sanitized : Lean.NameMap Lean.Name) (options✝ : Lean.Options) (nameStem2Idx✝ : Lean.NameMap ℕ) (userName2Sanitized✝ : Lean.NameMap Lean.Name) : ({ options := options, nameStem2Idx := nameStem2Idx, userName2Sanitized := userName2Sanitized } = { options := options✝, nameStem2Idx := nameStem2Idx✝, userName2Sanitized := userName2Sanitized✝ }) = (options = options✝ ∧ nameStem2Idx = nameStem2Idx✝ ∧ userName2Sanitized = userName2Sanitized✝)
• Lean.NameSanitizerState.mk.sizeOf_spec 📋 Lean.Hygiene
  (options : Lean.Options) (nameStem2Idx : Lean.NameMap ℕ) (userName2Sanitized : Lean.NameMap Lean.Name) : sizeOf { options := options, nameStem2Idx := nameStem2Idx, userName2Sanitized := userName2Sanitized } = 1 + sizeOf options + sizeOf nameStem2Idx + sizeOf userName2Sanitized
• Lean.LevelMVarId.name 📋 Lean.Level
  (self : Lean.LevelMVarId) : Lean.Name
• Lean.Expr.bindingName! 📋 Lean.Expr
  : Lean.Expr → Lean.Name
• Lean.Expr.constName 📋 Lean.Expr
  (e : Lean.Expr) : Lean.Name
• Lean.Expr.constName! 📋 Lean.Expr
  : Lean.Expr → Lean.Name
• Lean.Expr.ctorName 📋 Lean.Expr
  : Lean.Expr → String
• Lean.Expr.letName! 📋 Lean.Expr
  : Lean.Expr → Lean.Name
• Lean.FVarId.name 📋 Lean.Expr
  (self : Lean.FVarId) : Lean.Name
• Lean.MVarId.name 📋 Lean.Expr
  (self : Lean.MVarId) : Lean.Name
• Lean.Expr.constName? 📋 Lean.Expr
  : Lean.Expr → Option Lean.Name

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