Loogle!
Result
Found 3401 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
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
Lean.MacroScopesView → Lean.Name - Lean.MacroScopesView.mainModule Init.Prelude
Lean.MacroScopesView → Lean.Name - Lean.MacroScopesView.name Init.Prelude
Lean.MacroScopesView → Lean.Name - Lean.MacroScopesView.review 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.ParserDescr.const Init.Prelude
Lean.Name → Lean.ParserDescr - Lean.ParserDescr.parser Init.Prelude
Lean.Name → Lean.ParserDescr - Lean.Syntax.getId Init.Prelude
Lean.Syntax → Lean.Name - Lean.Macro.Context.mainModule Init.Prelude
Lean.Macro.Context → Lean.Name - Lean.Syntax.Preresolved.namespace Init.Prelude
Lean.Name → Lean.Syntax.Preresolved - Lean.Macro.addMacroScope Init.Prelude
Lean.Name → Lean.MacroM Lean.Name - Lean.Macro.hasDecl Init.Prelude
Lean.Name → Lean.MacroM Bool - 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.ParserDescr.cat Init.Prelude
Lean.Name → ℕ → Lean.ParserDescr - Lean.ParserDescr.unary Init.Prelude
Lean.Name → Lean.ParserDescr → Lean.ParserDescr - Lean.Syntax.matchesIdent Init.Prelude
Lean.Syntax → Lean.Name → Bool - Lean.Macro.Methods.getCurrNamespace Init.Prelude
Lean.Macro.Methods → Lean.MacroM Lean.Name - Lean.addMacroScope Init.Prelude
Lean.Name → Lean.Name → Lean.MacroScope → Lean.Name - Lean.Macro.resolveNamespace Init.Prelude
Lean.Name → Lean.MacroM (List Lean.Name) - Lean.Macro.trace Init.Prelude
Lean.Name → String → Lean.MacroM Unit - 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.ParserDescr.binary Init.Prelude
Lean.Name → Lean.ParserDescr → Lean.ParserDescr → Lean.ParserDescr - Lean.Macro.Methods.hasDecl Init.Prelude
Lean.Macro.Methods → Lean.Name → Lean.MacroM Bool - 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.Methods.resolveNamespace Init.Prelude
Lean.Macro.Methods → Lean.Name → Lean.MacroM (List Lean.Name) - Lean.Macro.State.traceMsgs Init.Prelude
Lean.Macro.State → List (Lean.Name × String) - Lean.MacroScopesView.mk Init.Prelude
Lean.Name → Lean.Name → Lean.Name → 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
String → String → String → String → String → Lean.Name - Lean.Syntax.ident Init.Prelude
Lean.SourceInfo → Substring → Lean.Name → List Lean.Syntax.Preresolved → Lean.Syntax - 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.Macro.Context.mk Init.Prelude
Lean.Macro.MethodsRef → Lean.Name → Lean.MacroScope → ℕ → ℕ → Lean.Syntax → Lean.Macro.Context - 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.MonadQuotation.addMacroScope Init.Prelude
{m : Type → Type} → [inst : Lean.MonadQuotation m] → [inst : Monad m] → Lean.Name → m Lean.Name - Lean.Name.mkStr8 Init.Prelude
String → String → String → String → String → String → String → String → Lean.Name - Lean.MonadQuotation.mk Init.Prelude
{m : Type → Type} → [toMonadRef : Lean.MonadRef m] → m Lean.MacroScope → m Lean.Name → ({α : Type} → m α → m α) → Lean.MonadQuotation m - 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.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_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.Syntax.ident.injEq Init.Core
∀ (info : Lean.SourceInfo) (rawVal : Substring) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved) (info_1 : Lean.SourceInfo) (rawVal_1 : Substring) (val_1 : Lean.Name) (preresolved_1 : List Lean.Syntax.Preresolved), (Lean.Syntax.ident info rawVal val preresolved = Lean.Syntax.ident info_1 rawVal_1 val_1 preresolved_1) = (info = info_1 ∧ rawVal = rawVal_1 ∧ val = val_1 ∧ preresolved = preresolved_1) - 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.mkCIdent Init.Meta
Lean.Name → Lean.Ident - Lean.mkIdent Init.Meta
Lean.Name → Lean.Ident - 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.TSyntax.getHygieneInfo Init.Meta
Lean.HygieneInfo → Lean.Name - Lean.TSyntax.getId Init.Meta
Lean.Ident → Lean.Name - Lean.TSyntax.getName Init.Meta
Lean.NameLit → Lean.Name - Lean.Name.toString.maybePseudoSyntax Init.Meta
Lean.Name → Bool - 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.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.getOptionalIdent? Init.Meta
Lean.Syntax → Option Lean.Name - Lean.Syntax.isNameLit? Init.Meta
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
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.Name.toString Init.Meta
Lean.Name → optParam Bool true → String - Lean.mkCIdentFrom Init.Meta
Lean.Syntax → Lean.Name → optParam Bool false → Lean.Ident - Lean.mkIdentFrom Init.Meta
Lean.Syntax → Lean.Name → optParam Bool false → Lean.Ident - Lean.HygieneInfo.mkIdent Init.Meta
Lean.HygieneInfo → Lean.Name → optParam Bool false → Lean.Ident - Lean.mkFreshId Init.Meta
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadNameGenerator m] → m Lean.Name - Lean.Syntax.mkCApp Init.Meta
Lean.Name → Lean.TSyntaxArray `term → Lean.Term - Lean.mkCIdentFromRef Init.Meta
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadRef m] → Lean.Name → optParam Bool false → m Lean.Syntax - Lean.mkIdentFromRef Init.Meta
{m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadRef m] → Lean.Name → optParam 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_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 - Lean.expandBrackedBinders Init.NotationExtra
Lean.Name → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax - Lean.expandExplicitBinders Init.NotationExtra
Lean.Name → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax - Dynamic.typeName Init.Dynamic
Dynamic → Lean.Name - 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.contains Lean.Data.KVMap
Lean.KVMap → 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
Lean.KVMap → Lean.Name → Lean.DataValue → Lean.DataValue - Lean.KVMap.insert Lean.Data.KVMap
Lean.KVMap → Lean.Name → Lean.DataValue → Lean.KVMap - Lean.KVMap.setBool Lean.Data.KVMap
Lean.KVMap → Lean.Name → Bool → Lean.KVMap - Lean.KVMap.setInt Lean.Data.KVMap
Lean.KVMap → Lean.Name → ℤ → Lean.KVMap - Lean.KVMap.setName Lean.Data.KVMap
Lean.KVMap → Lean.Name → Lean.Name → Lean.KVMap - Lean.KVMap.setNat Lean.Data.KVMap
Lean.KVMap → Lean.Name → ℕ → Lean.KVMap - Lean.KVMap.setString Lean.Data.KVMap
Lean.KVMap → Lean.Name → String → Lean.KVMap - Lean.KVMap.setSyntax Lean.Data.KVMap
Lean.KVMap → Lean.Name → Lean.Syntax → Lean.KVMap - Lean.KVMap.entries Lean.Data.KVMap
Lean.KVMap → List (Lean.Name × Lean.DataValue) - Lean.KVMap.mk Lean.Data.KVMap
List (Lean.Name × Lean.DataValue) → Lean.KVMap - Lean.KVMap.updateBool Lean.Data.KVMap
Lean.KVMap → Lean.Name → (Bool → Bool) → Lean.KVMap - Lean.KVMap.updateInt Lean.Data.KVMap
Lean.KVMap → Lean.Name → (ℤ → ℤ) → Lean.KVMap - Lean.KVMap.updateName Lean.Data.KVMap
Lean.KVMap → Lean.Name → (Lean.Name → Lean.Name) → Lean.KVMap - Lean.KVMap.updateNat Lean.Data.KVMap
Lean.KVMap → Lean.Name → (ℕ → ℕ) → Lean.KVMap - Lean.KVMap.updateString Lean.Data.KVMap
Lean.KVMap → Lean.Name → (String → String) → Lean.KVMap - Lean.KVMap.updateSyntax Lean.Data.KVMap
Lean.KVMap → Lean.Name → (Lean.Syntax → Lean.Syntax) → Lean.KVMap - Lean.KVMap.getBool Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam Bool false → Bool - Lean.KVMap.getName Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam Lean.Name Lean.Name.anonymous → Lean.Name - Lean.KVMap.getString Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam String "" → String - Lean.KVMap.getSyntax Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam 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} → [inst : Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → α → α - Lean.KVMap.get? Lean.Data.KVMap
{α : Type} → [inst : Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → Option α - Lean.KVMap.mergeBy Lean.Data.KVMap
(Lean.Name → Lean.DataValue → Lean.DataValue → Lean.DataValue) → Lean.KVMap → Lean.KVMap → Lean.KVMap - Lean.KVMap.set Lean.Data.KVMap
{α : Type} → [inst : Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → α → 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
Lean.KVMap → Lean.Name → optParam ℤ 0 → ℤ - Lean.KVMap.getNat Lean.Data.KVMap
Lean.KVMap → Lean.Name → optParam ℕ 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} → [inst : Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → (Option α → Option α) → Lean.KVMap - 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.KVMap.forIn Lean.Data.KVMap
{δ : Type w} → {m : Type w → Type w'} → [inst : Monad m] → Lean.KVMap → δ → (Lean.Name × Lean.DataValue → δ → m (ForInStep δ)) → m δ - Lean.KVMap.mk.injEq Lean.Data.KVMap
∀ (entries entries_1 : List (Lean.Name × Lean.DataValue)), ({ entries := entries } = { entries := entries_1 }) = (entries = entries_1) - 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.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.contains Lean.Data.NameMap
Lean.NameHashSet → Lean.Name → Bool - Lean.NameSSet.contains Lean.Data.NameMap
Lean.NameSSet → Lean.Name → Bool
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