Documentation

Lean.Data.Lsp.Extra

structure Lean.Lsp.WaitForDiagnosticsParams :

Type

uri : Lean.Lsp.DocumentUri
version : Nat

instance Lean.Lsp.instToJsonWaitForDiagnosticsParams :

Lean.ToJson Lean.Lsp.WaitForDiagnosticsParams

Equations

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

instance Lean.Lsp.instFromJsonWaitForDiagnosticsParams :

Lean.FromJson Lean.Lsp.WaitForDiagnosticsParams

Equations

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

structure Lean.Lsp.WaitForDiagnostics :

Type

instance Lean.Lsp.instFromJsonWaitForDiagnostics :

Lean.FromJson Lean.Lsp.WaitForDiagnostics

Equations

Lean.Lsp.instFromJsonWaitForDiagnostics = { fromJson? := fun j => pure { } }

instance Lean.Lsp.instToJsonWaitForDiagnostics :

Lean.ToJson Lean.Lsp.WaitForDiagnostics

Equations

Lean.Lsp.instToJsonWaitForDiagnostics = { toJson := fun o => Lean.Json.mkObj [] }

inductive Lean.Lsp.LeanFileProgressKind :

Type

processing: Lean.Lsp.LeanFileProgressKind
fatalError: Lean.Lsp.LeanFileProgressKind

instance Lean.Lsp.instBEqLeanFileProgressKind :

BEq Lean.Lsp.LeanFileProgressKind

Equations

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

instance Lean.Lsp.instInhabitedLeanFileProgressKind :

Inhabited Lean.Lsp.LeanFileProgressKind

Equations

Lean.Lsp.instInhabitedLeanFileProgressKind = { default := Lean.Lsp.LeanFileProgressKind.processing }

instance Lean.Lsp.instFromJsonLeanFileProgressKind :

Lean.FromJson Lean.Lsp.LeanFileProgressKind

Equations

Lean.Lsp.instFromJsonLeanFileProgressKind = { fromJson? := fun j => match Lean.Json.getNat? j with | Except.ok 1 => pure Lean.Lsp.LeanFileProgressKind.processing | Except.ok 2 => pure Lean.Lsp.LeanFileProgressKind.fatalError | x => throw (toString "unknown LeanFileProgressKind '" ++ toString j ++ toString "'") }

instance Lean.Lsp.instToJsonLeanFileProgressKind :

Lean.ToJson Lean.Lsp.LeanFileProgressKind

Equations

Lean.Lsp.instToJsonLeanFileProgressKind = { toJson := fun x => match x with | Lean.Lsp.LeanFileProgressKind.processing => 1 | Lean.Lsp.LeanFileProgressKind.fatalError => 2 }

structure Lean.Lsp.LeanFileProgressProcessingInfo :

Type

range : Lean.Lsp.Range
kind : Lean.Lsp.LeanFileProgressKind

instance Lean.Lsp.instToJsonLeanFileProgressProcessingInfo :

Lean.ToJson Lean.Lsp.LeanFileProgressProcessingInfo

Equations

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

instance Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo :

Lean.FromJson Lean.Lsp.LeanFileProgressProcessingInfo

Equations

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

structure Lean.Lsp.LeanFileProgressParams :

Type

textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
processing : Array Lean.Lsp.LeanFileProgressProcessingInfo

instance Lean.Lsp.instToJsonLeanFileProgressParams :

Lean.ToJson Lean.Lsp.LeanFileProgressParams

Equations

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

instance Lean.Lsp.instFromJsonLeanFileProgressParams :

Lean.FromJson Lean.Lsp.LeanFileProgressParams

Equations

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

structure Lean.Lsp.PlainGoalParams extends Lean.Lsp.TextDocumentPositionParams :

Type

instance Lean.Lsp.instFromJsonPlainGoalParams :

Lean.FromJson Lean.Lsp.PlainGoalParams

Equations

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

instance Lean.Lsp.instToJsonPlainGoalParams :

Lean.ToJson Lean.Lsp.PlainGoalParams

Equations

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

structure Lean.Lsp.PlainGoal :

Type

rendered : String
goals : Array String

instance Lean.Lsp.instToJsonPlainGoal :

Lean.ToJson Lean.Lsp.PlainGoal

Equations

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

instance Lean.Lsp.instFromJsonPlainGoal :

Lean.FromJson Lean.Lsp.PlainGoal

Equations

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

structure Lean.Lsp.PlainTermGoalParams extends Lean.Lsp.TextDocumentPositionParams :

Type

instance Lean.Lsp.instFromJsonPlainTermGoalParams :

Lean.FromJson Lean.Lsp.PlainTermGoalParams

Equations

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

instance Lean.Lsp.instToJsonPlainTermGoalParams :

Lean.ToJson Lean.Lsp.PlainTermGoalParams

Equations

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

structure Lean.Lsp.PlainTermGoal :

Type

goal : String
range : Lean.Lsp.Range

instance Lean.Lsp.instFromJsonPlainTermGoal :

Lean.FromJson Lean.Lsp.PlainTermGoal

Equations

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

instance Lean.Lsp.instToJsonPlainTermGoal :

Lean.ToJson Lean.Lsp.PlainTermGoal

Equations

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

structure Lean.Lsp.RpcRef :

Type

p : USize

instance Lean.Lsp.instBEqRpcRef :

BEq Lean.Lsp.RpcRef

Equations

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

instance Lean.Lsp.instFromJsonRpcRef :

Lean.FromJson Lean.Lsp.RpcRef

Equations

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

instance Lean.Lsp.instHashableRpcRef :

Hashable Lean.Lsp.RpcRef

Equations

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

instance Lean.Lsp.instToJsonRpcRef :

Lean.ToJson Lean.Lsp.RpcRef

Equations

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

instance Lean.Lsp.instToStringRpcRef :

ToString Lean.Lsp.RpcRef

Equations

Lean.Lsp.instToStringRpcRef = { toString := fun r => toString r.p }

structure Lean.Lsp.RpcConnectParams :

Type

uri : Lean.Lsp.DocumentUri

instance Lean.Lsp.instFromJsonRpcConnectParams :

Lean.FromJson Lean.Lsp.RpcConnectParams

Equations

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

instance Lean.Lsp.instToJsonRpcConnectParams :

Lean.ToJson Lean.Lsp.RpcConnectParams

Equations

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

structure Lean.Lsp.RpcConnected :

Type

sessionId : UInt64

instance Lean.Lsp.instToJsonRpcConnected :

Lean.ToJson Lean.Lsp.RpcConnected

Equations

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

instance Lean.Lsp.instFromJsonRpcConnected :

Lean.FromJson Lean.Lsp.RpcConnected

Equations

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

structure Lean.Lsp.RpcCallParams extends Lean.Lsp.TextDocumentPositionParams :

Type

sessionId : UInt64
method : Lean.Name
params : Lean.Json

instance Lean.Lsp.instToJsonRpcCallParams :

Lean.ToJson Lean.Lsp.RpcCallParams

Equations

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

instance Lean.Lsp.instFromJsonRpcCallParams :

Lean.FromJson Lean.Lsp.RpcCallParams

Equations

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

structure Lean.Lsp.RpcReleaseParams :

Type

instance Lean.Lsp.instToJsonRpcReleaseParams :

Lean.ToJson Lean.Lsp.RpcReleaseParams

Equations

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

instance Lean.Lsp.instFromJsonRpcReleaseParams :

Lean.FromJson Lean.Lsp.RpcReleaseParams

Equations

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

structure Lean.Lsp.RpcKeepAliveParams :

Type

uri : Lean.Lsp.DocumentUri
sessionId : UInt64

instance Lean.Lsp.instFromJsonRpcKeepAliveParams :

Lean.FromJson Lean.Lsp.RpcKeepAliveParams

Equations

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

instance Lean.Lsp.instToJsonRpcKeepAliveParams :

Lean.ToJson Lean.Lsp.RpcKeepAliveParams

Equations

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

structure Lean.Lsp.LineRange :

Type

start : Nat
end : Nat

instance Lean.Lsp.instInhabitedLineRange :

Inhabited Lean.Lsp.LineRange

Equations

Lean.Lsp.instInhabitedLineRange = { default := { start := default, end := default } }

instance Lean.Lsp.instReprLineRange :

Repr Lean.Lsp.LineRange

Equations

Lean.Lsp.instReprLineRange = { reprPrec := [anonymous] }

instance Lean.Lsp.instToJsonLineRange :

Lean.ToJson Lean.Lsp.LineRange

Equations

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

instance Lean.Lsp.instFromJsonLineRange :

Lean.FromJson Lean.Lsp.LineRange

Equations

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