Documentation

Lean.Elab.InfoTree.InlayHints

structure Lean.Elab.InlayHintLinkLocation :

module : Name
range : String.Range

structure Lean.Elab.InlayHintLabelPart :

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

inductive Lean.Elab.InlayHintLabel :

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

inductive Lean.Elab.InlayHintKind :

type : InlayHintKind
parameter : InlayHintKind

structure Lean.Elab.InlayHintTextEdit :

range : String.Range
newText : String

Instances For

Lean.Elab.instBEqInlayHintTextEdit

instance Lean.Elab.instBEqInlayHintTextEdit :

BEq InlayHintTextEdit

Equations

Lean.Elab.instBEqInlayHintTextEdit = { beq := Lean.Elab.beqInlayHintTextEdit✝ }

structure Lean.Elab.InlayHintInfo :

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 :

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

Instances For

Lean.Elab.instTypeNameInlayHint

instance Lean.Elab.instTypeNameInlayHint :

TypeName InlayHint

Equations

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

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

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 }