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

Equations

• Lean.Elab.instBEqInlayHintTextEdit = { beq := Lean.Elab.instBEqInlayHintTextEdit.beq }

def Lean.Elab.instBEqInlayHintTextEdit.beq : InlayHintTextEdit → InlayHintTextEdit → Bool

Equations

• Lean.Elab.instBEqInlayHintTextEdit.beq { range := a, newText := a_1 } { range := b, newText := b_1 } = (a == b && a_1 == b_1)
• Lean.Elab.instBEqInlayHintTextEdit.beq x✝¹ x✝ = false

structure Lean.Elab.InlayHintInfo : Type

• position : String.Pos.Raw
• 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.Raw
• 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

Equations

• Lean.Elab.instTypeNameInlayHint = Lean.Elab.inst✝

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

Equations

• i.toCustomInfo = { stx := Lean.Syntax.missing, value := Dynamic.mk i }

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

Equations

• Lean.Elab.InlayHint.ofCustomInfo? c = Dynamic.get? Lean.Elab.InlayHint c.value

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

Equations

• i.resolveDeferred = do let info ← i.deferredResolution i.toInlayHintInfo pure { toInlayHintInfo := info, lctx := i.lctx, deferredResolution := i.deferredResolution }