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.

structure Lean.Lsp.ImportInfo : Type

Information about a single import statement.

• module : String

  Name of the module that is imported.

• isPrivate : Bool

  Whether the module is being imported via private import.

• isAll : Bool

  Whether the module is being imported via import all.

• isMeta : Bool

  Whether the module is being imported via meta import.

def Lean.Lsp.instInhabitedImportInfo.default : ImportInfo

Equations

• Lean.Lsp.instInhabitedImportInfo.default = { module := default, isPrivate := default, isAll := default, isMeta := default }

instance Lean.Lsp.instInhabitedImportInfo : Inhabited ImportInfo

Equations

• Lean.Lsp.instInhabitedImportInfo = { default := Lean.Lsp.instInhabitedImportInfo.default }

instance Lean.Lsp.instToJsonImportInfo : ToJson ImportInfo

Equations

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

instance Lean.Lsp.instFromJsonImportInfo : FromJson ImportInfo

Equations

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

inductive Lean.Lsp.RefIdent : Type

Identifier of a reference.

• const (moduleName identName : String) : RefIdent

  Named identifier. These are used in all references that are globally available.

• fvar (moduleName id : String) : RefIdent

  Unnamed identifier. These are used for all local references.

instance Lean.Lsp.instBEqRefIdent : BEq RefIdent

Equations

• Lean.Lsp.instBEqRefIdent = { beq := Lean.Lsp.instBEqRefIdent.beq }

def Lean.Lsp.instBEqRefIdent.beq : RefIdent → RefIdent → Bool

Equations

• Lean.Lsp.instBEqRefIdent.beq (Lean.Lsp.RefIdent.const a a_1) (Lean.Lsp.RefIdent.const b b_1) = (a == b && a_1 == b_1)
• Lean.Lsp.instBEqRefIdent.beq (Lean.Lsp.RefIdent.fvar a a_1) (Lean.Lsp.RefIdent.fvar b b_1) = (a == b && a_1 == b_1)
• Lean.Lsp.instBEqRefIdent.beq x✝¹ x✝ = false

instance Lean.Lsp.instHashableRefIdent : Hashable RefIdent

Equations

• Lean.Lsp.instHashableRefIdent = { hash := Lean.Lsp.instHashableRefIdent.hash }

def Lean.Lsp.instHashableRefIdent.hash : RefIdent → UInt64

Equations

• Lean.Lsp.instHashableRefIdent.hash (Lean.Lsp.RefIdent.const a a_1) = mixHash (mixHash 0 (hash a)) (hash a_1)
• Lean.Lsp.instHashableRefIdent.hash (Lean.Lsp.RefIdent.fvar a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)

def Lean.Lsp.instInhabitedRefIdent.default : RefIdent

Equations

• Lean.Lsp.instInhabitedRefIdent.default = Lean.Lsp.RefIdent.const default default

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

Equations

• Lean.Lsp.instInhabitedRefIdent = { default := Lean.Lsp.instInhabitedRefIdent.default }

def Lean.Lsp.instOrdRefIdent.ord : RefIdent → RefIdent → Ordering

Equations

• Lean.Lsp.instOrdRefIdent.ord (Lean.Lsp.RefIdent.const a a_1) (Lean.Lsp.RefIdent.const b b_1) = (compare a b).then ((compare a_1 b_1).then Ordering.eq)
• Lean.Lsp.instOrdRefIdent.ord (Lean.Lsp.RefIdent.const a a_1) x✝ = Ordering.lt
• Lean.Lsp.instOrdRefIdent.ord x (Lean.Lsp.RefIdent.const b b_1) = Ordering.gt
• Lean.Lsp.instOrdRefIdent.ord (Lean.Lsp.RefIdent.fvar a a_1) (Lean.Lsp.RefIdent.fvar b b_1) = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

instance Lean.Lsp.instOrdRefIdent : Ord RefIdent

Equations

• Lean.Lsp.instOrdRefIdent = { compare := Lean.Lsp.instOrdRefIdent.ord }

inductive Lean.Lsp.RefIdent.RefIdentJsonRepr : Type

Shortened representation of RefIdent for more compact serialization.

• c (m n : String) : RefIdentJsonRepr

  Shortened representation of RefIdent.const for more compact serialization.

• f (m i : String) : RefIdentJsonRepr

  Shortened representation of RefIdent.fvar for more compact serialization.

def Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr.fromJson : Json → Except String RefIdentJsonRepr

Equations

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

instance Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr : FromJson RefIdentJsonRepr

Equations

• Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr = { fromJson? := Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr.fromJson }

def Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr.toJson : RefIdentJsonRepr → Json

Equations

• Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr.toJson (Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1) = Lean.Json.mkObj [("c", Lean.Json.mkObj [("m", Lean.toJson a), ("n", Lean.toJson a_1)])]
• Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr.toJson (Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1) = Lean.Json.mkObj [("f", Lean.Json.mkObj [("m", Lean.toJson a), ("i", Lean.toJson a_1)])]

instance Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : ToJson RefIdentJsonRepr

Equations

• Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr = { toJson := Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr.toJson }

def Lean.Lsp.RefIdent.toJsonRepr (id : RefIdent) : RefIdentJsonRepr

Converts id to its compact serialization representation.

Equations

• (Lean.Lsp.RefIdent.const a a_1).toJsonRepr = Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1
• (Lean.Lsp.RefIdent.fvar a a_1).toJsonRepr = Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1

def Lean.Lsp.RefIdent.fromJsonRepr (repr : RefIdentJsonRepr) : RefIdent

Converts repr to RefIdent.

Equations

• Lean.Lsp.RefIdent.fromJsonRepr (Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1) = Lean.Lsp.RefIdent.const a a_1
• Lean.Lsp.RefIdent.fromJsonRepr (Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1) = Lean.Lsp.RefIdent.fvar a a_1

def Lean.Lsp.RefIdent.fromJson? (s : Json) : Except String RefIdent

Converts RefIdent from a JSON for RefIdentJsonRepr.

Equations

• Lean.Lsp.RefIdent.fromJson? s = do let __do_lift ← Lean.fromJson? s pure (Lean.Lsp.RefIdent.fromJsonRepr __do_lift)

def Lean.Lsp.RefIdent.toJson (id : RefIdent) : Json

Converts RefIdent to a JSON for RefIdentJsonRepr.

Equations

• id.toJson = Lean.toJson id.toJsonRepr

instance Lean.Lsp.RefIdent.instFromJson : FromJson RefIdent

Equations

• Lean.Lsp.RefIdent.instFromJson = { fromJson? := Lean.Lsp.RefIdent.fromJson? }

instance Lean.Lsp.RefIdent.instToJson : ToJson RefIdent

Equations

• Lean.Lsp.RefIdent.instToJson = { toJson := Lean.Lsp.RefIdent.toJson }

structure Lean.Lsp.RefInfo.ParentDecl : Type

Information about the declaration surrounding a reference.

• name : String

  Name of the declaration surrounding a reference.

• range : Range

  Range of the declaration surrounding a reference.

• selectionRange : Range

  Selection range of the declaration surrounding a reference.

def Lean.Lsp.RefInfo.instToJsonParentDecl.toJson : ParentDecl → Json

Equations

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

instance Lean.Lsp.RefInfo.instToJsonParentDecl : ToJson ParentDecl

Equations

• Lean.Lsp.RefInfo.instToJsonParentDecl = { toJson := Lean.Lsp.RefInfo.instToJsonParentDecl.toJson }

structure Lean.Lsp.RefInfo.Location : Type

Denotes the range of a reference, as well as the parent declaration of the reference. If the reference is itself a declaration, then it contains no parent declaration.

• range : Range

  Range of the reference.

• parentDecl? : Option ParentDecl

  Parent declaration of the reference. none if the reference is itself a declaration.

instance Lean.Lsp.RefInfo.instInhabitedLocation : Inhabited Location

Equations

• Lean.Lsp.RefInfo.instInhabitedLocation = { default := Lean.Lsp.RefInfo.instInhabitedLocation.default }

def Lean.Lsp.RefInfo.instInhabitedLocation.default : Location

Equations

• Lean.Lsp.RefInfo.instInhabitedLocation.default = { range := default, parentDecl? := default }

structure Lean.Lsp.RefInfo : Type

Definition site and usage sites of a reference. Obtained from Lean.Server.RefInfo.

• definition? : Option Location

  Definition site of the reference. May be none when we cannot find a definition site.

• usages : Array Location

  Usage sites of the reference.

instance Lean.Lsp.instToJsonRefInfo : ToJson RefInfo

Equations

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

instance Lean.Lsp.instFromJsonRefInfo : FromJson RefInfo

Equations

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

def Lean.Lsp.ModuleRefs : Type

References from a single module/file

Equations

• Lean.Lsp.ModuleRefs = Std.TreeMap Lean.Lsp.RefIdent Lean.Lsp.RefInfo compare

instance Lean.Lsp.instEmptyCollectionModuleRefs : EmptyCollection ModuleRefs

Equations

• Lean.Lsp.instEmptyCollectionModuleRefs = Std.TreeMap.instEmptyCollection

instance Lean.Lsp.instForInModuleRefsProdRefIdentRefInfo {m : Type u_1 → Type u_2} : ForIn m ModuleRefs (RefIdent × RefInfo)

Equations

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

instance Lean.Lsp.instToJsonModuleRefs : ToJson ModuleRefs

Equations

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

instance Lean.Lsp.instFromJsonModuleRefs : FromJson ModuleRefs

Equations

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

structure Lean.Lsp.LeanILeanHeaderInfoParams : Type

Used in the $/lean/ileanHeaderInfo watchdog <- worker notifications. Contains the direct imports of the file managed by a worker.

• version : Nat

  Version of the file these imports are from.

• directImports : Array ImportInfo

  Direct imports of this file.

instance Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams : FromJson LeanILeanHeaderInfoParams

Equations

• Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams = { fromJson? := Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams.fromJson }

def Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams.fromJson : Json → Except String LeanILeanHeaderInfoParams

Equations

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

def Lean.Lsp.instToJsonLeanILeanHeaderInfoParams.toJson : LeanILeanHeaderInfoParams → Json

Equations

• Lean.Lsp.instToJsonLeanILeanHeaderInfoParams.toJson x✝ = Lean.Json.mkObj [[("version", Lean.toJson x✝.version)], [("directImports", Lean.toJson x✝.directImports)]].flatten

instance Lean.Lsp.instToJsonLeanILeanHeaderInfoParams : ToJson LeanILeanHeaderInfoParams

Equations

• Lean.Lsp.instToJsonLeanILeanHeaderInfoParams = { toJson := Lean.Lsp.instToJsonLeanILeanHeaderInfoParams.toJson }

structure Lean.Lsp.LeanIleanInfoParams : Type

Used in the $/lean/ileanInfoUpdate and $/lean/ileanInfoFinal watchdog <- worker notifications. Contains the definitions and references of the file managed by a worker.

• version : Nat

  Version of the file these references are from.

• references : ModuleRefs

  All references for the file.

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : FromJson LeanIleanInfoParams

Equations

• Lean.Lsp.instFromJsonLeanIleanInfoParams = { fromJson? := Lean.Lsp.instFromJsonLeanIleanInfoParams.fromJson }

def Lean.Lsp.instFromJsonLeanIleanInfoParams.fromJson : Json → Except String LeanIleanInfoParams

Equations

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

def Lean.Lsp.instToJsonLeanIleanInfoParams.toJson : LeanIleanInfoParams → Json

Equations

• Lean.Lsp.instToJsonLeanIleanInfoParams.toJson x✝ = Lean.Json.mkObj [[("version", Lean.toJson x✝.version)], [("references", Lean.toJson x✝.references)]].flatten

instance Lean.Lsp.instToJsonLeanIleanInfoParams : ToJson LeanIleanInfoParams

Equations

• Lean.Lsp.instToJsonLeanIleanInfoParams = { toJson := Lean.Lsp.instToJsonLeanIleanInfoParams.toJson }

structure Lean.Lsp.LeanImportClosureParams : Type

Used in the $/lean/importClosure watchdog <- worker notification. Contains the full import closure of the file managed by a worker.

• importClosure : Array DocumentUri

  Full import closure of the file.

def Lean.Lsp.instFromJsonLeanImportClosureParams.fromJson : Json → Except String LeanImportClosureParams

Equations

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

instance Lean.Lsp.instFromJsonLeanImportClosureParams : FromJson LeanImportClosureParams

Equations

• Lean.Lsp.instFromJsonLeanImportClosureParams = { fromJson? := Lean.Lsp.instFromJsonLeanImportClosureParams.fromJson }

instance Lean.Lsp.instToJsonLeanImportClosureParams : ToJson LeanImportClosureParams

Equations

• Lean.Lsp.instToJsonLeanImportClosureParams = { toJson := Lean.Lsp.instToJsonLeanImportClosureParams.toJson }

def Lean.Lsp.instToJsonLeanImportClosureParams.toJson : LeanImportClosureParams → Json

Equations

• Lean.Lsp.instToJsonLeanImportClosureParams.toJson x✝ = Lean.Json.mkObj [[("importClosure", Lean.toJson x✝.importClosure)]].flatten

structure Lean.Lsp.LeanStaleDependencyParams : Type

Used in the $/lean/importClosure watchdog -> worker notification. Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.

• staleDependency : DocumentUri

  The dependency that is stale.

def Lean.Lsp.instFromJsonLeanStaleDependencyParams.fromJson : Json → Except String LeanStaleDependencyParams

Equations

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

instance Lean.Lsp.instFromJsonLeanStaleDependencyParams : FromJson LeanStaleDependencyParams

Equations

• Lean.Lsp.instFromJsonLeanStaleDependencyParams = { fromJson? := Lean.Lsp.instFromJsonLeanStaleDependencyParams.fromJson }

def Lean.Lsp.instToJsonLeanStaleDependencyParams.toJson : LeanStaleDependencyParams → Json

Equations

• Lean.Lsp.instToJsonLeanStaleDependencyParams.toJson x✝ = Lean.Json.mkObj [[("staleDependency", Lean.toJson x✝.staleDependency)]].flatten

instance Lean.Lsp.instToJsonLeanStaleDependencyParams : ToJson LeanStaleDependencyParams

Equations

• Lean.Lsp.instToJsonLeanStaleDependencyParams = { toJson := Lean.Lsp.instToJsonLeanStaleDependencyParams.toJson }

inductive Lean.Lsp.OpenNamespace : Type

LSP type for Lean.OpenDecl.

• allExcept («namespace» : Name) (exceptions : Array Name) : OpenNamespace

  All declarations in «namespace» are opened, except for exceptions.

• renamed («from» to : Name) : OpenNamespace

  The declaration «from» is renamed to to.

def Lean.Lsp.instFromJsonOpenNamespace.fromJson : Json → Except String OpenNamespace

Equations

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

instance Lean.Lsp.instFromJsonOpenNamespace : FromJson OpenNamespace

Equations

• Lean.Lsp.instFromJsonOpenNamespace = { fromJson? := Lean.Lsp.instFromJsonOpenNamespace.fromJson }

instance Lean.Lsp.instToJsonOpenNamespace : ToJson OpenNamespace

Equations

• Lean.Lsp.instToJsonOpenNamespace = { toJson := Lean.Lsp.instToJsonOpenNamespace.toJson }

def Lean.Lsp.instToJsonOpenNamespace.toJson : OpenNamespace → Json

Equations

• Lean.Lsp.instToJsonOpenNamespace.toJson (Lean.Lsp.OpenNamespace.allExcept a a_1) = Lean.Json.mkObj [("allExcept", Lean.Json.mkObj [("namespace", Lean.toJson a), ("exceptions", Lean.toJson a_1)])]
• Lean.Lsp.instToJsonOpenNamespace.toJson (Lean.Lsp.OpenNamespace.renamed a a_1) = Lean.Json.mkObj [("renamed", Lean.Json.mkObj [("from", Lean.toJson a), ("to", Lean.toJson a_1)])]

structure Lean.Lsp.LeanModuleQuery : Type

Query in the $/lean/queryModule watchdog <- worker request.

• identifier : String

  Identifier (potentially partial) to query.

• openNamespaces : Array OpenNamespace

  Namespaces that are open at the position of identifier. Used for accurately matching declarations against identifier in context.

instance Lean.Lsp.instFromJsonLeanModuleQuery : FromJson LeanModuleQuery

Equations

• Lean.Lsp.instFromJsonLeanModuleQuery = { fromJson? := Lean.Lsp.instFromJsonLeanModuleQuery.fromJson }

def Lean.Lsp.instFromJsonLeanModuleQuery.fromJson : Json → Except String LeanModuleQuery

Equations

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

instance Lean.Lsp.instToJsonLeanModuleQuery : ToJson LeanModuleQuery

Equations

• Lean.Lsp.instToJsonLeanModuleQuery = { toJson := Lean.Lsp.instToJsonLeanModuleQuery.toJson }

def Lean.Lsp.instToJsonLeanModuleQuery.toJson : LeanModuleQuery → Json

Equations

• Lean.Lsp.instToJsonLeanModuleQuery.toJson x✝ = Lean.Json.mkObj [[("identifier", Lean.toJson x✝.identifier)], [("openNamespaces", Lean.toJson x✝.openNamespaces)]].flatten

structure Lean.Lsp.LeanQueryModuleParams : Type

Used in the $/lean/queryModule watchdog <- worker request, which is used by the worker to extract information from the .ilean information in the watchdog.

• sourceRequestID : JsonRpc.RequestID

  The request ID in the context of which this worker -> watchdog request was emitted. Used for cancelling this request in the watchdog.

• queries : Array LeanModuleQuery

  Module queries for extracting .ilean information in the watchdog.

def Lean.Lsp.instFromJsonLeanQueryModuleParams.fromJson : Json → Except String LeanQueryModuleParams

Equations

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

instance Lean.Lsp.instFromJsonLeanQueryModuleParams : FromJson LeanQueryModuleParams

Equations

• Lean.Lsp.instFromJsonLeanQueryModuleParams = { fromJson? := Lean.Lsp.instFromJsonLeanQueryModuleParams.fromJson }

def Lean.Lsp.instToJsonLeanQueryModuleParams.toJson : LeanQueryModuleParams → Json

Equations

• Lean.Lsp.instToJsonLeanQueryModuleParams.toJson x✝ = Lean.Json.mkObj [[("sourceRequestID", Lean.toJson x✝.sourceRequestID)], [("queries", Lean.toJson x✝.queries)]].flatten

instance Lean.Lsp.instToJsonLeanQueryModuleParams : ToJson LeanQueryModuleParams

Equations

• Lean.Lsp.instToJsonLeanQueryModuleParams = { toJson := Lean.Lsp.instToJsonLeanQueryModuleParams.toJson }

structure Lean.Lsp.LeanIdentifier : Type

Result entry of a module query.

• module : Name

  Module that decl is defined in.

• decl : Name

  Full name of the declaration that matches the query.

• isExactMatch : Bool

  Whether this decl matched the query exactly.

instance Lean.Lsp.instFromJsonLeanIdentifier : FromJson LeanIdentifier

Equations

• Lean.Lsp.instFromJsonLeanIdentifier = { fromJson? := Lean.Lsp.instFromJsonLeanIdentifier.fromJson }

def Lean.Lsp.instFromJsonLeanIdentifier.fromJson : Json → Except String LeanIdentifier

Equations

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

instance Lean.Lsp.instToJsonLeanIdentifier : ToJson LeanIdentifier

Equations

• Lean.Lsp.instToJsonLeanIdentifier = { toJson := Lean.Lsp.instToJsonLeanIdentifier.toJson }

def Lean.Lsp.instToJsonLeanIdentifier.toJson : LeanIdentifier → Json

Equations

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

@[reducible, inline]

abbrev Lean.Lsp.LeanQueriedModule : Type

Result for a single module query. Identifiers in the response are sorted descendingly by how well they match the query.

Equations

• Lean.Lsp.LeanQueriedModule = Array Lean.Lsp.LeanIdentifier

structure Lean.Lsp.LeanQueryModuleResponse : Type

Response for the $/lean/queryModule watchdog <- worker request.

• queryResults : Array LeanQueriedModule

  Results for each query in LeanQueryModuleParams. Positions correspond to queries in the parameter of the request.

def Lean.Lsp.instFromJsonLeanQueryModuleResponse.fromJson : Json → Except String LeanQueryModuleResponse

Equations

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

instance Lean.Lsp.instFromJsonLeanQueryModuleResponse : FromJson LeanQueryModuleResponse

Equations

• Lean.Lsp.instFromJsonLeanQueryModuleResponse = { fromJson? := Lean.Lsp.instFromJsonLeanQueryModuleResponse.fromJson }

def Lean.Lsp.instToJsonLeanQueryModuleResponse.toJson : LeanQueryModuleResponse → Json

Equations

• Lean.Lsp.instToJsonLeanQueryModuleResponse.toJson x✝ = Lean.Json.mkObj [[("queryResults", Lean.toJson x✝.queryResults)]].flatten

instance Lean.Lsp.instToJsonLeanQueryModuleResponse : ToJson LeanQueryModuleResponse

Equations

• Lean.Lsp.instToJsonLeanQueryModuleResponse = { toJson := Lean.Lsp.instToJsonLeanQueryModuleResponse.toJson }

instance Lean.Lsp.instInhabitedLeanQueryModuleResponse : Inhabited LeanQueryModuleResponse

Equations

• Lean.Lsp.instInhabitedLeanQueryModuleResponse = { default := Lean.Lsp.instInhabitedLeanQueryModuleResponse.default }

def Lean.Lsp.instInhabitedLeanQueryModuleResponse.default : LeanQueryModuleResponse

Equations

• Lean.Lsp.instInhabitedLeanQueryModuleResponse.default = { queryResults := default }

structure Lean.Lsp.LeanDeclIdent : Type

Name of a declaration in a given module.

• module : Name

  Name of the module that this identifier is in.

• decl : Name

  Name of the declaration.

def Lean.Lsp.instFromJsonLeanDeclIdent.fromJson : Json → Except String LeanDeclIdent

Equations

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

instance Lean.Lsp.instFromJsonLeanDeclIdent : FromJson LeanDeclIdent

Equations

• Lean.Lsp.instFromJsonLeanDeclIdent = { fromJson? := Lean.Lsp.instFromJsonLeanDeclIdent.fromJson }

instance Lean.Lsp.instToJsonLeanDeclIdent : ToJson LeanDeclIdent

Equations

• Lean.Lsp.instToJsonLeanDeclIdent = { toJson := Lean.Lsp.instToJsonLeanDeclIdent.toJson }

def Lean.Lsp.instToJsonLeanDeclIdent.toJson : LeanDeclIdent → Json

Equations

• Lean.Lsp.instToJsonLeanDeclIdent.toJson x✝ = Lean.Json.mkObj [[("module", Lean.toJson x✝.module)], [("decl", Lean.toJson x✝.decl)]].flatten

structure Lean.Lsp.LeanLocationLinkextends Lean.Lsp.LocationLink : Type

LocationLink with additional meta-data that allows the watchdog to resolve the range of this LocationLink. This is necessary because the position information from the .olean may be stale (e.g. if the user has edited the file that the definition is from, but neither saved or built it), while file workers sync their current reference information into the watchdog using ilean info notifications, which is up-to-date.

• originSelectionRange? : Option Range
• targetUri : DocumentUri
• targetRange : Range
• targetSelectionRange : Range
• ident? : Option LeanDeclIdent

  Identifier that caused this location link.

• isDefault : Bool

  Whether this location link was generated by a fallback handler. If the file worker can't produce any non-fallback location links, the watchdog tries again using its reference information from the ileans and ilean updates.

def Lean.Lsp.instFromJsonLeanLocationLink.fromJson : Json → Except String LeanLocationLink

Equations

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

instance Lean.Lsp.instFromJsonLeanLocationLink : FromJson LeanLocationLink

Equations

• Lean.Lsp.instFromJsonLeanLocationLink = { fromJson? := Lean.Lsp.instFromJsonLeanLocationLink.fromJson }

def Lean.Lsp.instToJsonLeanLocationLink.toJson : LeanLocationLink → Json

Equations

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

instance Lean.Lsp.instToJsonLeanLocationLink : ToJson LeanLocationLink

Equations

• Lean.Lsp.instToJsonLeanLocationLink = { toJson := Lean.Lsp.instToJsonLeanLocationLink.toJson }