Lean.Data.Lsp.Internal

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

source

inductive Lean.Lsp.RefIdent:

Type

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

source

instance Lean.Lsp.instBEqRefIdent:

BEq Lean.Lsp.RefIdent

Equations

Lean.Lsp.instBEqRefIdent = { beq := [anonymous] }

source

instance Lean.Lsp.instHashableRefIdent:

Hashable Lean.Lsp.RefIdent

Equations

Lean.Lsp.instHashableRefIdent = { hash := [anonymous] }

source

instance Lean.Lsp.instInhabitedRefIdent:

Inhabited Lean.Lsp.RefIdent

Equations

Lean.Lsp.instInhabitedRefIdent = { default := Lean.Lsp.RefIdent.const default }

source

def Lean.Lsp.RefIdent.toString:

Lean.Lsp.RefIdent → String

Equations

One or more equations did not get rendered due to their size.

source

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

Except String Lean.Lsp.RefIdent

Equations

One or more equations did not get rendered due to their size.

source

structure Lean.Lsp.RefInfo:

Type

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

source

instance Lean.Lsp.instToJsonRefInfo:

Lean.ToJson Lean.Lsp.RefInfo

Equations

One or more equations did not get rendered due to their size.

source

instance Lean.Lsp.instFromJsonRefInfo:

Lean.FromJson Lean.Lsp.RefInfo

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Lsp.ModuleRefs:

Type

References from a single module/file

Equations

Lean.Lsp.ModuleRefs = Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefInfo

source

instance Lean.Lsp.instToJsonModuleRefs:

Lean.ToJson Lean.Lsp.ModuleRefs

Equations

One or more equations did not get rendered due to their size.

source

instance Lean.Lsp.instFromJsonModuleRefs:

Lean.FromJson Lean.Lsp.ModuleRefs

Equations

One or more equations did not get rendered due to their size.

source

structure Lean.Lsp.LeanIleanInfoParams:

Type

Version of the file these references are from.
version : Nat
references : Lean.Lsp.ModuleRefs

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

Contains the file's definitions and references.

source

instance Lean.Lsp.instFromJsonLeanIleanInfoParams:

Lean.FromJson Lean.Lsp.LeanIleanInfoParams

Equations

Lean.Lsp.instFromJsonLeanIleanInfoParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonLeanIleanInfoParams:

Lean.ToJson Lean.Lsp.LeanIleanInfoParams

Equations

Lean.Lsp.instToJsonLeanIleanInfoParams = { toJson := [anonymous] }