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