def Lean.String.charactersIn (a b : String) : Bool

Returns true if the characters of a occur in b in order (not necessarily contiguously), compared case-insensitively via Char.toLower.

This function assumes that a and b have size at most USize.size, which should be a safe assumption.

Equations

• Lean.String.charactersIn a b = Lean.String.charactersIn.goFastScalar✝ a b a.utf8ByteSize.toUSize b.utf8ByteSize.toUSize 0 0 ⋯ ⋯

inductive Lean.Server.Completion.HoverInfo : Type

• after : HoverInfo
• inside (delta : Nat) : HoverInfo

structure Lean.Server.Completion.ContextualizedCompletionInfo : Type

• hoverInfo : HoverInfo
• ctx : Elab.ContextInfo
• info : Elab.CompletionInfo

def Lean.Server.Completion.minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name) : Name

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Completion.unfoldDefinitionGuarded? (e : Expr) : MetaM (Option Expr)

Equations

• Lean.Server.Completion.unfoldDefinitionGuarded? e = tryCatch (Lean.Meta.unfoldDefinition? e) fun (x : Lean.Exception) => pure none

def Lean.Server.Completion.getDotCompletionTypeNames (type : Expr) : MetaM (Array Name)

Get type names for resolving id in s.id x₁ ... xₙ notation.

Equations

• Lean.Server.Completion.getDotCompletionTypeNames type = do let __do_lift ← (Lean.Server.Completion.getDotCompletionTypeNames.visit✝ type).run #[] pure __do_lift.snd

def Lean.Server.Completion.getDotIdCompletionTypeNames (type : Expr) : MetaM (Array Name)

Gets type names for resolving id in .id x₁ ... xₙ notation. The process mimics the dotted identifier notation elaboration procedure at Lean.Elab.App. Catches and ignores all errors, so no need to run this within try/catch.

Equations

• Lean.Server.Completion.getDotIdCompletionTypeNames type = do let __do_lift ← (Lean.Server.Completion.getDotIdCompletionTypeNames.visit✝ type).run #[] pure __do_lift.snd