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.

instance Lean.Lsp.instInhabitedImportInfo : Inhabited ImportInfo

Equations

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

def Lean.Lsp.instInhabitedImportInfo.default : ImportInfo

Equations

• Lean.Lsp.instInhabitedImportInfo.default = { module := default, isPrivate := default, isAll := default, isMeta := 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.

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.instBEqRefIdent : BEq RefIdent

Equations

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

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)

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

Equations

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

def Lean.Lsp.instInhabitedRefIdent.default : RefIdent

Equations

• Lean.Lsp.instInhabitedRefIdent.default = Lean.Lsp.RefIdent.const default 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 }

instance Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : ToJson RefIdentJsonRepr

Equations

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

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)])]

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.DeclInfo : Type

Position information for a declaration. Inlined to reduce memory consumption.

• rangeStartPosLine : Nat

  Start line of range.

• rangeStartPosCharacter : Nat

  Start character of range.

• rangeEndPosLine : Nat

  End line of range.

• rangeEndPosCharacter : Nat

  End character of range.

• selectionRangeStartPosLine : Nat

  Start line of selection range.

• selectionRangeStartPosCharacter : Nat

  Start character of selection range.

• selectionRangeEndPosLine : Nat

  End line of selection range.

• selectionRangeEndPosCharacter : Nat

  End character of selection range.

def Lean.Lsp.DeclInfo.ofDeclarationRanges (r : DeclarationRanges) : DeclInfo

Converts a set of DeclarationRanges to a DeclInfo.

Equations

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

def Lean.Lsp.DeclInfo.range (i : DeclInfo) : Range

Range of this parent decl.

Equations

• i.range = { start := { line := i.rangeStartPosLine, character := i.rangeStartPosCharacter }, «end» := { line := i.rangeEndPosLine, character := i.rangeEndPosCharacter } }

def Lean.Lsp.DeclInfo.selectionRange (i : DeclInfo) : Range

Selection range of this parent decl.

Equations

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

instance Lean.Lsp.instToJsonDeclInfo : ToJson DeclInfo

Equations

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

instance Lean.Lsp.instFromJsonDeclInfo : FromJson DeclInfo

Equations

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

def Lean.Lsp.Decls : Type

Declarations of a file with associated position information.

Equations

• Lean.Lsp.Decls = Std.TreeMap String Lean.Lsp.DeclInfo compare

instance Lean.Lsp.instEmptyCollectionDecls : EmptyCollection Decls

Equations

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

instance Lean.Lsp.instForInIdDeclsProdStringDeclInfo : ForIn Id Decls (String × DeclInfo)

Equations

• Lean.Lsp.instForInIdDeclsProdStringDeclInfo = Std.TreeMap.instForInProdOfMonad

instance Lean.Lsp.instToJsonDecls : ToJson Decls

Equations

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

instance Lean.Lsp.instFromJsonDecls : FromJson Decls

Equations

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

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. The position information is inlined to reduce memory consumption.

• mk' :: (
• startPosLine : Nat

  Start line of the range of this location.

• startPosCharacter : Nat

  Start character of the range of this location.

• endPosLine : Nat

  End line of the range of this location.

• endPosCharacter : Nat

  End character of the range of this location.

• parentDecl : String

  Parent declaration of the reference. Empty string if the reference is itself a declaration. We do not use Option for memory consumption reasons.

• )

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 = { startPosLine := default, startPosCharacter := default, endPosLine := default, endPosCharacter := default, parentDecl := default }

def Lean.Lsp.RefInfo.Location.mk (range : Range) (parentDecl? : Option String) : Location

Creates a RefInfo.Location.

Equations

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

def Lean.Lsp.RefInfo.Location.range (l : Location) : Range

Range of this location.

Equations

• l.range = { start := { line := l.startPosLine, character := l.startPosCharacter }, «end» := { line := l.endPosLine, character := l.endPosCharacter } }

def Lean.Lsp.RefInfo.Location.parentDecl? (l : Location) : Option String

Name of the parent declaration of this location.

Equations

• l.parentDecl? = if l.parentDecl.isEmpty = true then none else some l.parentDecl

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.instForInModuleRefsProdRefIdentRefInfoOfMonad {m : Type u_1 → Type u_2} [Monad m] : 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.

instance Lean.Lsp.instToJsonLeanILeanHeaderInfoParams : ToJson LeanILeanHeaderInfoParams

Equations

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

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

structure Lean.Lsp.LeanILeanHeaderSetupInfoParams : Type

Used in the $/lean/ileanHeaderSetupInfo watchdog <- worker notifications. Contains status information about lake setup-file.

• version : Nat

  Version of the file these imports are from.

• isSetupFailure : Bool

  Whether setting up the header using lake setup-file has failed.

def Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams.fromJson : Json → Except String LeanILeanHeaderSetupInfoParams

Equations

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

instance Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams : FromJson LeanILeanHeaderSetupInfoParams

Equations

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

instance Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams : ToJson LeanILeanHeaderSetupInfoParams

Equations

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

def Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams.toJson : LeanILeanHeaderSetupInfoParams → Json

Equations

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

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.

• decls : Decls

  All decls for the file.

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

Equations

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

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : FromJson LeanIleanInfoParams

Equations

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

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

Equations

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

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.

instance Lean.Lsp.instFromJsonLeanImportClosureParams : FromJson LeanImportClosureParams

Equations

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

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.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.

instance Lean.Lsp.instFromJsonLeanStaleDependencyParams : FromJson LeanStaleDependencyParams

Equations

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

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

Equations

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

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.

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

instance Lean.Lsp.instToJsonLeanModuleQuery : ToJson LeanModuleQuery

Equations

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

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.

instance Lean.Lsp.instFromJsonLeanQueryModuleParams : FromJson LeanQueryModuleParams

Equations

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

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

Equations

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

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.

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.instFromJsonLeanIdentifier : FromJson LeanIdentifier

Equations

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

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

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 }

@[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 }

def Lean.Lsp.instInhabitedLeanQueryModuleResponse.default : LeanQueryModuleResponse

Equations

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

instance Lean.Lsp.instInhabitedLeanQueryModuleResponse : Inhabited LeanQueryModuleResponse

Equations

• Lean.Lsp.instInhabitedLeanQueryModuleResponse = { default := Lean.Lsp.instInhabitedLeanQueryModuleResponse.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 }