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.
- const: Lake.Name → Lean.Lsp.RefIdent
- fvar: Lean.FVarId → Lean.Lsp.RefIdent
Instances For
- definition : Option Lean.Lsp.Range
- usages : Array Lean.Lsp.Range
Instances For
- 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.