structure Lean.Elab.InlayHintLinkLocation : Type

• module : Name
• range : String.Range

structure Lean.Elab.InlayHintLabelPart : Type

• value : String
• tooltip? : Option String
• location? : Option InlayHintLinkLocation

inductive Lean.Elab.InlayHintLabel : Type

• name (n : String) : InlayHintLabel
• parts (p : Array InlayHintLabelPart) : InlayHintLabel

inductive Lean.Elab.InlayHintKind : Type

• type : InlayHintKind
• parameter : InlayHintKind

structure Lean.Elab.InlayHintTextEdit : Type

• range : String.Range
• newText : String

instance Lean.Elab.instBEqInlayHintTextEdit : BEq InlayHintTextEdit

structure Lean.Elab.InlayHintInfo : Type

• position : String.Pos
• label : InlayHintLabel
• kind? : Option InlayHintKind
• textEdits : Array InlayHintTextEdit
• tooltip? : Option String
• paddingLeft : Bool
• paddingRight : Bool

structure Lean.Elab.InlayHintextends Lean.Elab.InlayHintInfo : Type

• position : String.Pos
• label : InlayHintLabel
• kind? : Option InlayHintKind
• textEdits : Array InlayHintTextEdit
• tooltip? : Option String
• paddingLeft : Bool
• paddingRight : Bool
• lctx : LocalContext
• deferredResolution : InlayHintInfo → MetaM InlayHintInfo

instance Lean.Elab.instTypeNameInlayHint : TypeName InlayHint

def Lean.Elab.InlayHint.toCustomInfo (i : InlayHint) : CustomInfo

def Lean.Elab.InlayHint.ofCustomInfo? (c : CustomInfo) : Option InlayHint

def Lean.Elab.InlayHint.resolveDeferred (i : InlayHint) : MetaM InlayHint