@[reducible, inline]

abbrev Lapis.Protocol.Messages.ServerInfo : Type

Equations

• Lapis.Protocol.Messages.ServerInfo = Lapis.Protocol.Generated.ServerInfo

structure Lapis.Protocol.Messages.DidOpenTextDocumentParams : Type

• textDocument : Types.TextDocumentItem

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedDidOpenTextDocumentParams : Inhabited DidOpenTextDocumentParams

Equations

• Lapis.Protocol.Messages.instInhabitedDidOpenTextDocumentParams = { default := Lapis.Protocol.Messages.instInhabitedDidOpenTextDocumentParams.default }

def Lapis.Protocol.Messages.instInhabitedDidOpenTextDocumentParams.default : DidOpenTextDocumentParams

Equations

• Lapis.Protocol.Messages.instInhabitedDidOpenTextDocumentParams.default = { textDocument := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonDidOpenTextDocumentParams : Lean.ToJson DidOpenTextDocumentParams

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonDidOpenTextDocumentParams : Lean.FromJson DidOpenTextDocumentParams

Equations

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

@[reducible, inline]

abbrev Lapis.Protocol.Messages.DidCloseTextDocumentParams : Type

Equations

• Lapis.Protocol.Messages.DidCloseTextDocumentParams = Lapis.Protocol.Generated.DidCloseTextDocumentParams

@[reducible, inline]

abbrev Lapis.Protocol.Messages.DidSaveTextDocumentParams : Type

Equations

• Lapis.Protocol.Messages.DidSaveTextDocumentParams = Lapis.Protocol.Generated.DidSaveTextDocumentParams

@[reducible, inline]

abbrev Lapis.Protocol.Messages.HoverParams : Type

Equations

• Lapis.Protocol.Messages.HoverParams = Lapis.Protocol.Generated.HoverParams

@[reducible, inline]

abbrev Lapis.Protocol.Messages.CompletionTriggerKind : Type

Equations

• Lapis.Protocol.Messages.CompletionTriggerKind = Lapis.Protocol.Generated.CompletionTriggerKind

@[reducible, inline]

abbrev Lapis.Protocol.Messages.CompletionContext : Type

Equations

• Lapis.Protocol.Messages.CompletionContext = Lapis.Protocol.Generated.CompletionContext

@[reducible, inline]

abbrev Lapis.Protocol.Messages.CompletionParams : Type

Equations

• Lapis.Protocol.Messages.CompletionParams = Lapis.Protocol.Generated.CompletionParams

@[reducible, inline]

abbrev Lapis.Protocol.Messages.CompletionItemKind : Type

Equations

• Lapis.Protocol.Messages.CompletionItemKind = Lapis.Protocol.Generated.CompletionItemKind

@[reducible, inline]

abbrev Lapis.Protocol.Messages.ConfigurationItem : Type

Equations

• Lapis.Protocol.Messages.ConfigurationItem = Lapis.Protocol.Generated.ConfigurationItem

@[reducible, inline]

abbrev Lapis.Protocol.Messages.ConfigurationParams : Type

Equations

• Lapis.Protocol.Messages.ConfigurationParams = Lapis.Protocol.Generated.ConfigurationParams

@[reducible, inline]

abbrev Lapis.Protocol.Messages.ReferenceContext : Type

Equations

• Lapis.Protocol.Messages.ReferenceContext = Lapis.Protocol.Generated.ReferenceContext

structure Lapis.Protocol.Messages.InitializeParams : Type

• processId : Option Int
• rootUri : Option Types.DocumentUri
• capabilities : Capabilities.ClientCapabilities
• trace : Option String

def Lapis.Protocol.Messages.instInhabitedInitializeParams.default : InitializeParams

Equations

• Lapis.Protocol.Messages.instInhabitedInitializeParams.default = { processId := default, rootUri := default, trace := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedInitializeParams : Inhabited InitializeParams

Equations

• Lapis.Protocol.Messages.instInhabitedInitializeParams = { default := Lapis.Protocol.Messages.instInhabitedInitializeParams.default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonInitializeParams : Lean.ToJson InitializeParams

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonInitializeParams : Lean.FromJson InitializeParams

Equations

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

structure Lapis.Protocol.Messages.InitializeResult : Type

• capabilities : Capabilities.ServerCapabilities
• serverInfo : Option ServerInfo

def Lapis.Protocol.Messages.instInhabitedInitializeResult.default : InitializeResult

Equations

• Lapis.Protocol.Messages.instInhabitedInitializeResult.default = { capabilities := default, serverInfo := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedInitializeResult : Inhabited InitializeResult

Equations

• Lapis.Protocol.Messages.instInhabitedInitializeResult = { default := Lapis.Protocol.Messages.instInhabitedInitializeResult.default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonInitializeResult : Lean.ToJson InitializeResult

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonInitializeResult : Lean.FromJson InitializeResult

Equations

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

structure Lapis.Protocol.Messages.TextDocumentContentChangeEvent : Type

• range : Option Types.Range
• text : String

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedTextDocumentContentChangeEvent : Inhabited TextDocumentContentChangeEvent

Equations

• Lapis.Protocol.Messages.instInhabitedTextDocumentContentChangeEvent = { default := Lapis.Protocol.Messages.instInhabitedTextDocumentContentChangeEvent.default }

def Lapis.Protocol.Messages.instInhabitedTextDocumentContentChangeEvent.default : TextDocumentContentChangeEvent

Equations

• Lapis.Protocol.Messages.instInhabitedTextDocumentContentChangeEvent.default = { range := default, text := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonTextDocumentContentChangeEvent : Lean.ToJson TextDocumentContentChangeEvent

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonTextDocumentContentChangeEvent : Lean.FromJson TextDocumentContentChangeEvent

Equations

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

structure Lapis.Protocol.Messages.DidChangeTextDocumentParams : Type

• textDocument : Types.VersionedTextDocumentIdentifier
• contentChanges : Array TextDocumentContentChangeEvent

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedDidChangeTextDocumentParams : Inhabited DidChangeTextDocumentParams

Equations

• Lapis.Protocol.Messages.instInhabitedDidChangeTextDocumentParams = { default := Lapis.Protocol.Messages.instInhabitedDidChangeTextDocumentParams.default }

def Lapis.Protocol.Messages.instInhabitedDidChangeTextDocumentParams.default : DidChangeTextDocumentParams

Equations

• Lapis.Protocol.Messages.instInhabitedDidChangeTextDocumentParams.default = { textDocument := default, contentChanges := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonDidChangeTextDocumentParams : Lean.ToJson DidChangeTextDocumentParams

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonDidChangeTextDocumentParams : Lean.FromJson DidChangeTextDocumentParams

Equations

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

structure Lapis.Protocol.Messages.Hover : Type

• contents : Types.MarkupContent
• range : Option Types.Range

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedHover : Inhabited Hover

Equations

• Lapis.Protocol.Messages.instInhabitedHover = { default := Lapis.Protocol.Messages.instInhabitedHover.default }

def Lapis.Protocol.Messages.instInhabitedHover.default : Hover

Equations

• Lapis.Protocol.Messages.instInhabitedHover.default = { contents := default, range := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonHover : Lean.ToJson Hover

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonHover : Lean.FromJson Hover

Equations

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

structure Lapis.Protocol.Messages.PublishDiagnosticsParams : Type

• uri : Types.DocumentUri
• version : Option Int
• diagnostics : Array Types.Diagnostic

def Lapis.Protocol.Messages.instInhabitedPublishDiagnosticsParams.default : PublishDiagnosticsParams

Equations

• Lapis.Protocol.Messages.instInhabitedPublishDiagnosticsParams.default = { uri := default, version := default, diagnostics := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedPublishDiagnosticsParams : Inhabited PublishDiagnosticsParams

Equations

• Lapis.Protocol.Messages.instInhabitedPublishDiagnosticsParams = { default := Lapis.Protocol.Messages.instInhabitedPublishDiagnosticsParams.default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonPublishDiagnosticsParams : Lean.ToJson PublishDiagnosticsParams

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonPublishDiagnosticsParams : Lean.FromJson PublishDiagnosticsParams

Equations

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

structure Lapis.Protocol.Messages.CompletionItem : Type

• label : String
• kind : Option CompletionItemKind
• detail : Option String
• documentation : Option Types.MarkupContent
• insertText : Option String

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedCompletionItem : Inhabited CompletionItem

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionItem = { default := Lapis.Protocol.Messages.instInhabitedCompletionItem.default }

def Lapis.Protocol.Messages.instInhabitedCompletionItem.default : CompletionItem

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionItem.default = { label := default, kind := default, detail := default, documentation := default, insertText := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonCompletionItem : Lean.ToJson CompletionItem

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonCompletionItem : Lean.FromJson CompletionItem

Equations

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

structure Lapis.Protocol.Messages.CompletionList : Type

• isIncomplete : Bool
• items : Array CompletionItem

def Lapis.Protocol.Messages.instInhabitedCompletionList.default : CompletionList

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionList.default = { isIncomplete := default, items := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedCompletionList : Inhabited CompletionList

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionList = { default := Lapis.Protocol.Messages.instInhabitedCompletionList.default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonCompletionList : Lean.ToJson CompletionList

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonCompletionList : Lean.FromJson CompletionList

Equations

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

@[reducible, inline]

abbrev Lapis.Protocol.Messages.DefinitionParams : Type

Equations

• Lapis.Protocol.Messages.DefinitionParams = Lapis.Protocol.Types.TextDocumentPositionParams

structure Lapis.Protocol.Messages.ReferenceParams : Type

• textDocument : Types.TextDocumentIdentifier
• position : Types.Position
• context : ReferenceContext

@[implicit_reducible]

instance Lapis.Protocol.Messages.instInhabitedReferenceParams : Inhabited ReferenceParams

Equations

• Lapis.Protocol.Messages.instInhabitedReferenceParams = { default := Lapis.Protocol.Messages.instInhabitedReferenceParams.default }

def Lapis.Protocol.Messages.instInhabitedReferenceParams.default : ReferenceParams

Equations

• Lapis.Protocol.Messages.instInhabitedReferenceParams.default = { textDocument := default, position := default, context := default }

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonReferenceParams : Lean.ToJson ReferenceParams

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonReferenceParams : Lean.FromJson ReferenceParams

Equations

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

structure Lapis.Protocol.Messages.DidChangeConfigurationParams (ConfigType : Type) : Type

Parameters for workspace/didChangeConfiguration notification

• settings : ConfigType

@[implicit_reducible]

instance Lapis.Protocol.Messages.instToJsonDidChangeConfigurationParams {ConfigType : Type} [Lean.ToJson ConfigType] : Lean.ToJson (DidChangeConfigurationParams ConfigType)

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Messages.instFromJsonDidChangeConfigurationParams {ConfigType : Type} [Lean.FromJson ConfigType] : Lean.FromJson (DidChangeConfigurationParams ConfigType)

Equations

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