Loogle!
Result
Found 1232 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
Lean.MacroScopesView → Lean.Name - Lean.Name.eraseMacroScopes Init.Prelude
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
String → Lean.Name - Lean.Name.mkStr1 Init.Prelude
String → Lean.Name - Lean.Name.simpMacroScopes Init.Prelude
Lean.Name → Lean.Name - Lean.Syntax.Preresolved.namespace Init.Prelude
Lean.Name → Lean.Syntax.Preresolved - Lean.Name.append Init.Prelude
Lean.Name → Lean.Name → Lean.Name - Lean.Name.appendCore Init.Prelude
Lean.Name → Lean.Name → Lean.Name - Lean.Name.mkNum Init.Prelude
Lean.Name → ℕ → Lean.Name - Lean.Name.mkStr Init.Prelude
Lean.Name → String → Lean.Name - Lean.Name.mkStr2 Init.Prelude
String → String → Lean.Name - Lean.Name.num Init.Prelude
Lean.Name → ℕ → Lean.Name - Lean.Name.str Init.Prelude
Lean.Name → String → Lean.Name - Lean.Macro.Methods.getCurrNamespace Init.Prelude
Lean.Macro.Methods → Lean.MacroM Lean.Name - Lean.Macro.resolveNamespace Init.Prelude
Lean.Name → Lean.MacroM (List Lean.Name) - Lean.Name.below Init.Prelude
{motive : Lean.Name → Sort u} → Lean.Name → Sort (max 1 u) - Lean.Name.beq Init.Prelude
Lean.Name → Lean.Name → Bool - Lean.Name.ibelow Init.Prelude
{motive : Lean.Name → Prop} → Lean.Name → Prop - Lean.Name.mkStr3 Init.Prelude
String → String → String → Lean.Name - Lean.Name.mkStr4 Init.Prelude
String → String → String → String → Lean.Name - Lean.Macro.Methods.resolveNamespace Init.Prelude
Lean.Macro.Methods → Lean.Name → Lean.MacroM (List Lean.Name) - Lean.Name.mkStr5 Init.Prelude
String → String → String → String → String → Lean.Name - 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 - namedPattern Init.Prelude
{α : Sort u} → (x a : α) → x = a → α - 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.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_1 : Lean.Name) (i_1 : ℕ), (pre.num i = pre_1.num i_1) = (pre = pre_1 ∧ i = i_1) - 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) - Lean.NameGenerator Init.MetaTypes
Type - Lean.instInhabitedNameGenerator Init.MetaTypes
Inhabited Lean.NameGenerator - Lean.NameGenerator.idx Init.MetaTypes
Lean.NameGenerator → ℕ - Lean.NameGenerator.namePrefix Init.MetaTypes
Lean.NameGenerator → Lean.Name - Lean.NameGenerator.mk Init.MetaTypes
Lean.Name → ℕ → Lean.NameGenerator - Lean.NameGenerator.mk.injEq Init.MetaTypes
∀ (namePrefix : Lean.Name) (idx : ℕ) (namePrefix_1 : Lean.Name) (idx_1 : ℕ), ({ namePrefix := namePrefix, idx := idx } = { namePrefix := namePrefix_1, idx := idx_1 }) = (namePrefix = namePrefix_1 ∧ idx = idx_1) - 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
String → Lean.Name - Substring.toName Init.Meta
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
Lean.NameGenerator → Lean.Name - Lean.NameGenerator.next Init.Meta
Lean.NameGenerator → Lean.NameGenerator - Lean.TSyntax.getName Init.Meta
Lean.NameLit → Lean.Name - Lean.Name.toString.maybePseudoSyntax Init.Meta
Lean.Name → Bool - Lean.MonadNameGenerator Init.Meta
(Type → Type) → Type - Lean.Name.appendAfter Init.Meta
Lean.Name → String → Lean.Name - Lean.Name.appendBefore Init.Meta
Lean.Name → String → Lean.Name - Lean.Name.appendIndexAfter Init.Meta
Lean.Name → ℕ → Lean.Name - Lean.Name.escapePart Init.Meta
String → Option String - Lean.Name.instLawfulBEq Init.Meta
LawfulBEq Lean.Name - Lean.Name.reprPrec Init.Meta
Lean.Name → ℕ → Lean.Format - Lean.Syntax.decodeNameLit Init.Meta
String → Option Lean.Name - Lean.Syntax.isNameLit? Init.Meta
Lean.Syntax → Option Lean.Name - Lean.Syntax.splitNameLit Init.Meta
Substring → List Substring - Lean.TSyntax.instCoeNameLitTerm Init.Meta
Coe Lean.NameLit Lean.Term - Lean.Name.toStringWithSep.maybeEscape Init.Meta
Bool → String → String - 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
Lean.Name → (Lean.Name → Lean.Name) → Lean.Name - Lean.Name.replacePrefix Init.Meta
Lean.Name → Lean.Name → Lean.Name → Lean.Name - Lean.Name.toStringWithSep Init.Meta
String → Bool → Lean.Name → String - Lean.NameGenerator.mkChild Init.Meta
Lean.NameGenerator → Lean.NameGenerator × Lean.NameGenerator - Lean.Name.toString Init.Meta
Lean.Name → optParam Bool true → String - Lean.Syntax.mkNameLit Init.Meta
String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.NameLit - Lean.MonadNameGenerator.getNGen Init.Meta
{m : Type → Type} → [self : Lean.MonadNameGenerator m] → m Lean.NameGenerator - 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} → m Lean.NameGenerator → (Lean.NameGenerator → m Unit) → Lean.MonadNameGenerator m - Lean.monadNameGeneratorLift Init.Meta
(m n : Type → Type) → [inst : MonadLift m n] → [inst : 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_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_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 - System.FilePath.fileName Init.System.FilePath
System.FilePath → Option String - System.FilePath.withFileName Init.System.FilePath
System.FilePath → String → System.FilePath - IO.FS.DirEntry.fileName Init.System.IO
IO.FS.DirEntry → String - IO.FS.rename Init.System.IO
System.FilePath → System.FilePath → IO Unit - TypeName Init.Dynamic
Type u → Type - Dynamic.typeName Init.Dynamic
Dynamic → Lean.Name - instNonemptyTypeName Init.Dynamic
∀ {α : Type u_1}, Nonempty (TypeName α) - TypeName.mk Init.Dynamic
(α : Type u) → Lean.Name → TypeName α - TypeName.typeName Init.Dynamic
(α : Type u_1) → [inst : TypeName α] → Lean.Name - Lean.DataValue.ofName Lean.Data.KVMap
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
Lean.KVMap → Lean.Name → Lean.Name → Lean.KVMap - Lean.KVMap.updateName Lean.Data.KVMap
Lean.KVMap → Lean.Name → (Lean.Name → Lean.Name) → Lean.KVMap - Lean.KVMap.getName Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam 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_1 : Lean.Name), (Lean.DataValue.ofName v = Lean.DataValue.ofName v_1) = (v = v_1) - 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.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
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
Lean.Name → Lean.Name → Bool - Lean.Name.quickCmp Lean.Data.Name
Lean.Name → Lean.Name → Ordering - Lean.Name.quickCmpAux Lean.Data.Name
Lean.Name → Lean.Name → Ordering - Lean.Name.quickLt Lean.Data.Name
Lean.Name → Lean.Name → Bool - Lean.Name.updatePrefix Lean.Data.Name
Lean.Name → Lean.Name → Lean.Name - Lean.Name.anyS Lean.Data.Name
Lean.Name → (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
Lean.NameHashSet → Lean.Name → Bool - Lean.NameSSet.contains Lean.Data.NameMap
Lean.NameSSet → Lean.Name → Bool - Lean.NameSSet.insert Lean.Data.NameMap
Lean.NameSSet → Lean.Name → Lean.NameSSet - Lean.NameSet.append Lean.Data.NameMap
Lean.NameSet → Lean.NameSet → Lean.NameSet - Lean.NameSet.contains Lean.Data.NameMap
Lean.NameSet → Lean.Name → Bool - Lean.NameSet.insert Lean.Data.NameMap
Lean.NameSet → Lean.Name → Lean.NameSet - Lean.NameMap.instEmptyCollection Lean.Data.NameMap
(α : Type) → EmptyCollection (Lean.NameMap α) - Lean.NameMap.instInhabited Lean.Data.NameMap
(α : Type) → Inhabited (Lean.NameMap α) - Lean.NameMap.contains Lean.Data.NameMap
{α : Type} → Lean.NameMap α → Lean.Name → Bool - Lean.NameHashSet.insert Lean.Data.NameMap
Lean.NameHashSet → Lean.Name → Lean.HashSet Lean.Name - Lean.NameMap.find? Lean.Data.NameMap
{α : Type} → Lean.NameMap α → Lean.Name → Option α - Lean.NameSet.instForInName Lean.Data.NameMap
{m : Type u_1 → Type u_2} → ForIn m Lean.NameSet Lean.Name - Lean.NameMap.insert Lean.Data.NameMap
{α : Type} → Lean.NameMap α → Lean.Name → α → Lean.RBMap Lean.Name α Lean.Name.quickCmp - 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
Lean.OptionDecl → Lean.Name - Lean.Option.name Lean.Data.Options
{α : Type} → 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
Lean.Options → Bool - Lean.getPPPrivateNames Lean.PrettyPrinter.Delaborator.Options
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
Lean.Options → Bool - Lean.NameSanitizerState.options Lean.Hygiene
Lean.NameSanitizerState → Lean.Options - Lean.pp.sanitizeNames Lean.Hygiene
Lean.Option Bool - Lean.NameSanitizerState.nameStem2Idx Lean.Hygiene
Lean.NameSanitizerState → Lean.NameMap ℕ - Lean.NameSanitizerState.userName2Sanitized Lean.Hygiene
Lean.NameSanitizerState → Lean.NameMap Lean.Name - Lean.sanitizeName Lean.Hygiene
Lean.Name → StateM Lean.NameSanitizerState Lean.Name - Lean.NameSanitizerState.mk Lean.Hygiene
Lean.Options → Lean.NameMap ℕ → Lean.NameMap Lean.Name → Lean.NameSanitizerState - Lean.NameSanitizerState.mk.injEq Lean.Hygiene
∀ (options : Lean.Options) (nameStem2Idx : Lean.NameMap ℕ) (userName2Sanitized : Lean.NameMap Lean.Name) (options_1 : Lean.Options) (nameStem2Idx_1 : Lean.NameMap ℕ) (userName2Sanitized_1 : Lean.NameMap Lean.Name), ({ options := options, nameStem2Idx := nameStem2Idx, userName2Sanitized := userName2Sanitized } = { options := options_1, nameStem2Idx := nameStem2Idx_1, userName2Sanitized := userName2Sanitized_1 }) = (options = options_1 ∧ nameStem2Idx = nameStem2Idx_1 ∧ userName2Sanitized = userName2Sanitized_1) - 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
Lean.LevelMVarId → Lean.Name - Lean.Expr.bindingName! Lean.Expr
Lean.Expr → Lean.Name - Lean.Expr.constName Lean.Expr
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
Lean.FVarId → Lean.Name - Lean.MVarId.name Lean.Expr
Lean.MVarId → Lean.Name - Lean.Expr.constName? Lean.Expr
Lean.Expr → Option Lean.Name - Lean.Expr.getForallBinderNames Lean.Expr
Lean.Expr → List Lean.Name - Lean.mkRecName Lean.Declaration
Lean.Name → Lean.Name - Lean.ConstantInfo.name Lean.Declaration
Lean.ConstantInfo → Lean.Name - Lean.ConstantVal.name Lean.Declaration
Lean.ConstantVal → Lean.Name
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