This file contains types for communication between the watchdog and the workers. These messages are not visible externally to users of the LSP server.

Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON.

inductive Lean.Lsp.RefIdent : Type

• const: Lake.Name → Lean.Lsp.RefIdent
• fvar: Lean.FVarId → Lean.Lsp.RefIdent

instance Lean.Lsp.instBEqRefIdent : BEq Lean.Lsp.RefIdent

instance Lean.Lsp.instHashableRefIdent : Hashable Lean.Lsp.RefIdent

instance Lean.Lsp.instInhabitedRefIdent : Inhabited Lean.Lsp.RefIdent

def Lean.Lsp.RefIdent.toString : Lean.Lsp.RefIdent → String

def Lean.Lsp.RefIdent.fromString (s : String) : Except String Lean.Lsp.RefIdent

structure Lean.Lsp.RefInfo : Type

• definition : Option Lean.Lsp.Range
• usages : Array Lean.Lsp.Range

instance Lean.Lsp.instToJsonRefInfo : Lean.ToJson Lean.Lsp.RefInfo

instance Lean.Lsp.instFromJsonRefInfo : Lean.FromJson Lean.Lsp.RefInfo

def Lean.Lsp.ModuleRefs : Type

References from a single module/file

instance Lean.Lsp.instToJsonModuleRefs : Lean.ToJson Lean.Lsp.ModuleRefs

instance Lean.Lsp.instFromJsonModuleRefs : Lean.FromJson Lean.Lsp.ModuleRefs

structure Lean.Lsp.LeanIleanInfoParams : Type

• version : Nat

  Version of the file these references are from.

• references : Lean.Lsp.ModuleRefs

$/lean/ileanInfoUpdate and $/lean/ileanInfoFinal watchdog<-worker notifications.

Contains the file's definitions and references.

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : Lean.FromJson Lean.Lsp.LeanIleanInfoParams

instance Lean.Lsp.instToJsonLeanIleanInfoParams : Lean.ToJson Lean.Lsp.LeanIleanInfoParams