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 }

instance Lapis.Protocol.Messages.instInhabitedInitializeParams : Inhabited InitializeParams

Equations

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

instance Lapis.Protocol.Messages.instReprInitializeParams : Repr InitializeParams

Equations

• Lapis.Protocol.Messages.instReprInitializeParams = { reprPrec := Lapis.Protocol.Messages.instReprInitializeParams.repr }

def Lapis.Protocol.Messages.instReprInitializeParams.repr : InitializeParams → Nat → Std.Format

Equations

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

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

Equations

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

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

• name : String
• version : Option String

def Lapis.Protocol.Messages.instInhabitedServerInfo.default : ServerInfo

Equations

• Lapis.Protocol.Messages.instInhabitedServerInfo.default = { name := default, version := default }

instance Lapis.Protocol.Messages.instInhabitedServerInfo : Inhabited ServerInfo

Equations

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

instance Lapis.Protocol.Messages.instReprServerInfo : Repr ServerInfo

Equations

• Lapis.Protocol.Messages.instReprServerInfo = { reprPrec := Lapis.Protocol.Messages.instReprServerInfo.repr }

def Lapis.Protocol.Messages.instReprServerInfo.repr : ServerInfo → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonServerInfo : Lean.ToJson ServerInfo

Equations

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

instance Lapis.Protocol.Messages.instFromJsonServerInfo : Lean.FromJson ServerInfo

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

instance Lapis.Protocol.Messages.instInhabitedInitializeResult : Inhabited InitializeResult

Equations

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

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

Equations

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

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

Equations

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

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

• textDocument : Types.TextDocumentItem

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

Equations

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

instance Lapis.Protocol.Messages.instInhabitedDidOpenTextDocumentParams : Inhabited DidOpenTextDocumentParams

Equations

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

def Lapis.Protocol.Messages.instReprDidOpenTextDocumentParams.repr : DidOpenTextDocumentParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprDidOpenTextDocumentParams : Repr DidOpenTextDocumentParams

Equations

• Lapis.Protocol.Messages.instReprDidOpenTextDocumentParams = { reprPrec := Lapis.Protocol.Messages.instReprDidOpenTextDocumentParams.repr }

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

Equations

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

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

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

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 }

def Lapis.Protocol.Messages.instReprTextDocumentContentChangeEvent.repr : TextDocumentContentChangeEvent → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprTextDocumentContentChangeEvent : Repr TextDocumentContentChangeEvent

Equations

• Lapis.Protocol.Messages.instReprTextDocumentContentChangeEvent = { reprPrec := Lapis.Protocol.Messages.instReprTextDocumentContentChangeEvent.repr }

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

Equations

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

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

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 }

def Lapis.Protocol.Messages.instReprDidChangeTextDocumentParams.repr : DidChangeTextDocumentParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprDidChangeTextDocumentParams : Repr DidChangeTextDocumentParams

Equations

• Lapis.Protocol.Messages.instReprDidChangeTextDocumentParams = { reprPrec := Lapis.Protocol.Messages.instReprDidChangeTextDocumentParams.repr }

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

Equations

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

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

• textDocument : Types.TextDocumentIdentifier

instance Lapis.Protocol.Messages.instInhabitedDidCloseTextDocumentParams : Inhabited DidCloseTextDocumentParams

Equations

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

def Lapis.Protocol.Messages.instInhabitedDidCloseTextDocumentParams.default : DidCloseTextDocumentParams

Equations

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

instance Lapis.Protocol.Messages.instReprDidCloseTextDocumentParams : Repr DidCloseTextDocumentParams

Equations

• Lapis.Protocol.Messages.instReprDidCloseTextDocumentParams = { reprPrec := Lapis.Protocol.Messages.instReprDidCloseTextDocumentParams.repr }

def Lapis.Protocol.Messages.instReprDidCloseTextDocumentParams.repr : DidCloseTextDocumentParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonDidCloseTextDocumentParams : Lean.ToJson DidCloseTextDocumentParams

Equations

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

instance Lapis.Protocol.Messages.instFromJsonDidCloseTextDocumentParams : Lean.FromJson DidCloseTextDocumentParams

Equations

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

structure Lapis.Protocol.Messages.DidSaveTextDocumentParams : Type

• textDocument : Types.TextDocumentIdentifier
• text : Option String

instance Lapis.Protocol.Messages.instInhabitedDidSaveTextDocumentParams : Inhabited DidSaveTextDocumentParams

Equations

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

def Lapis.Protocol.Messages.instInhabitedDidSaveTextDocumentParams.default : DidSaveTextDocumentParams

Equations

• Lapis.Protocol.Messages.instInhabitedDidSaveTextDocumentParams.default = { textDocument := default, text := default }

instance Lapis.Protocol.Messages.instReprDidSaveTextDocumentParams : Repr DidSaveTextDocumentParams

Equations

• Lapis.Protocol.Messages.instReprDidSaveTextDocumentParams = { reprPrec := Lapis.Protocol.Messages.instReprDidSaveTextDocumentParams.repr }

def Lapis.Protocol.Messages.instReprDidSaveTextDocumentParams.repr : DidSaveTextDocumentParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonDidSaveTextDocumentParams : Lean.ToJson DidSaveTextDocumentParams

Equations

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

instance Lapis.Protocol.Messages.instFromJsonDidSaveTextDocumentParams : Lean.FromJson DidSaveTextDocumentParams

Equations

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

structure Lapis.Protocol.Messages.HoverParams : Type

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

def Lapis.Protocol.Messages.instInhabitedHoverParams.default : HoverParams

Equations

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

instance Lapis.Protocol.Messages.instInhabitedHoverParams : Inhabited HoverParams

Equations

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

def Lapis.Protocol.Messages.instReprHoverParams.repr : HoverParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprHoverParams : Repr HoverParams

Equations

• Lapis.Protocol.Messages.instReprHoverParams = { reprPrec := Lapis.Protocol.Messages.instReprHoverParams.repr }

instance Lapis.Protocol.Messages.instToJsonHoverParams : Lean.ToJson HoverParams

Equations

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

instance Lapis.Protocol.Messages.instFromJsonHoverParams : Lean.FromJson HoverParams

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

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

Equations

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

instance Lapis.Protocol.Messages.instInhabitedHover : Inhabited Hover

Equations

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

instance Lapis.Protocol.Messages.instReprHover : Repr Hover

Equations

• Lapis.Protocol.Messages.instReprHover = { reprPrec := Lapis.Protocol.Messages.instReprHover.repr }

def Lapis.Protocol.Messages.instReprHover.repr : Hover → Nat → Std.Format

Equations

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

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

Equations

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

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

instance Lapis.Protocol.Messages.instInhabitedPublishDiagnosticsParams : Inhabited PublishDiagnosticsParams

Equations

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

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

Equations

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

instance Lapis.Protocol.Messages.instReprPublishDiagnosticsParams : Repr PublishDiagnosticsParams

Equations

• Lapis.Protocol.Messages.instReprPublishDiagnosticsParams = { reprPrec := Lapis.Protocol.Messages.instReprPublishDiagnosticsParams.repr }

def Lapis.Protocol.Messages.instReprPublishDiagnosticsParams.repr : PublishDiagnosticsParams → Nat → Std.Format

Equations

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

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

Equations

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

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

Equations

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

inductive Lapis.Protocol.Messages.CompletionTriggerKind : Type

• invoked : CompletionTriggerKind
• triggerCharacter : CompletionTriggerKind
• triggerForIncompleteCompletions : CompletionTriggerKind

def Lapis.Protocol.Messages.instInhabitedCompletionTriggerKind.default : CompletionTriggerKind

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionTriggerKind.default = Lapis.Protocol.Messages.CompletionTriggerKind.invoked

instance Lapis.Protocol.Messages.instInhabitedCompletionTriggerKind : Inhabited CompletionTriggerKind

Equations

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

def Lapis.Protocol.Messages.instBEqCompletionTriggerKind.beq : CompletionTriggerKind → CompletionTriggerKind → Bool

Equations

• Lapis.Protocol.Messages.instBEqCompletionTriggerKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lapis.Protocol.Messages.instBEqCompletionTriggerKind : BEq CompletionTriggerKind

Equations

• Lapis.Protocol.Messages.instBEqCompletionTriggerKind = { beq := Lapis.Protocol.Messages.instBEqCompletionTriggerKind.beq }

instance Lapis.Protocol.Messages.instReprCompletionTriggerKind : Repr CompletionTriggerKind

Equations

• Lapis.Protocol.Messages.instReprCompletionTriggerKind = { reprPrec := Lapis.Protocol.Messages.instReprCompletionTriggerKind.repr }

def Lapis.Protocol.Messages.instReprCompletionTriggerKind.repr : CompletionTriggerKind → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonCompletionTriggerKind : Lean.ToJson CompletionTriggerKind

Equations

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

instance Lapis.Protocol.Messages.instFromJsonCompletionTriggerKind : Lean.FromJson CompletionTriggerKind

Equations

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

structure Lapis.Protocol.Messages.CompletionContext : Type

• triggerKind : CompletionTriggerKind
• triggerCharacter : Option String

instance Lapis.Protocol.Messages.instInhabitedCompletionContext : Inhabited CompletionContext

Equations

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

def Lapis.Protocol.Messages.instInhabitedCompletionContext.default : CompletionContext

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionContext.default = { triggerKind := default, triggerCharacter := default }

instance Lapis.Protocol.Messages.instReprCompletionContext : Repr CompletionContext

Equations

• Lapis.Protocol.Messages.instReprCompletionContext = { reprPrec := Lapis.Protocol.Messages.instReprCompletionContext.repr }

def Lapis.Protocol.Messages.instReprCompletionContext.repr : CompletionContext → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonCompletionContext : Lean.ToJson CompletionContext

Equations

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

instance Lapis.Protocol.Messages.instFromJsonCompletionContext : Lean.FromJson CompletionContext

Equations

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

structure Lapis.Protocol.Messages.CompletionParams : Type

• textDocument : Types.TextDocumentIdentifier
• position : Types.Position
• context : Option CompletionContext

instance Lapis.Protocol.Messages.instInhabitedCompletionParams : Inhabited CompletionParams

Equations

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

def Lapis.Protocol.Messages.instInhabitedCompletionParams.default : CompletionParams

Equations

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

instance Lapis.Protocol.Messages.instReprCompletionParams : Repr CompletionParams

Equations

• Lapis.Protocol.Messages.instReprCompletionParams = { reprPrec := Lapis.Protocol.Messages.instReprCompletionParams.repr }

def Lapis.Protocol.Messages.instReprCompletionParams.repr : CompletionParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonCompletionParams : Lean.ToJson CompletionParams

Equations

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

instance Lapis.Protocol.Messages.instFromJsonCompletionParams : Lean.FromJson CompletionParams

Equations

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

inductive Lapis.Protocol.Messages.CompletionItemKind : Type

• text : CompletionItemKind
• method : CompletionItemKind
• function : CompletionItemKind
• constructor : CompletionItemKind
• field : CompletionItemKind
• variable : CompletionItemKind
• class_ : CompletionItemKind
• interface : CompletionItemKind
• module : CompletionItemKind
• property : CompletionItemKind
• unit : CompletionItemKind
• value : CompletionItemKind
• enum : CompletionItemKind
• keyword : CompletionItemKind
• snippet : CompletionItemKind
• color : CompletionItemKind
• file : CompletionItemKind
• reference : CompletionItemKind
• folder : CompletionItemKind
• enumMember : CompletionItemKind
• constant : CompletionItemKind
• struct : CompletionItemKind
• event : CompletionItemKind
• operator : CompletionItemKind
• typeParameter : CompletionItemKind

def Lapis.Protocol.Messages.instInhabitedCompletionItemKind.default : CompletionItemKind

Equations

• Lapis.Protocol.Messages.instInhabitedCompletionItemKind.default = Lapis.Protocol.Messages.CompletionItemKind.text

instance Lapis.Protocol.Messages.instInhabitedCompletionItemKind : Inhabited CompletionItemKind

Equations

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

def Lapis.Protocol.Messages.instBEqCompletionItemKind.beq : CompletionItemKind → CompletionItemKind → Bool

Equations

• Lapis.Protocol.Messages.instBEqCompletionItemKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lapis.Protocol.Messages.instBEqCompletionItemKind : BEq CompletionItemKind

Equations

• Lapis.Protocol.Messages.instBEqCompletionItemKind = { beq := Lapis.Protocol.Messages.instBEqCompletionItemKind.beq }

def Lapis.Protocol.Messages.instReprCompletionItemKind.repr : CompletionItemKind → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprCompletionItemKind : Repr CompletionItemKind

Equations

• Lapis.Protocol.Messages.instReprCompletionItemKind = { reprPrec := Lapis.Protocol.Messages.instReprCompletionItemKind.repr }

instance Lapis.Protocol.Messages.instToJsonCompletionItemKind : Lean.ToJson CompletionItemKind

Equations

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

instance Lapis.Protocol.Messages.instFromJsonCompletionItemKind : Lean.FromJson CompletionItemKind

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

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 }

instance Lapis.Protocol.Messages.instReprCompletionItem : Repr CompletionItem

Equations

• Lapis.Protocol.Messages.instReprCompletionItem = { reprPrec := Lapis.Protocol.Messages.instReprCompletionItem.repr }

def Lapis.Protocol.Messages.instReprCompletionItem.repr : CompletionItem → Nat → Std.Format

Equations

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

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

Equations

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

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 }

instance Lapis.Protocol.Messages.instInhabitedCompletionList : Inhabited CompletionList

Equations

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

instance Lapis.Protocol.Messages.instReprCompletionList : Repr CompletionList

Equations

• Lapis.Protocol.Messages.instReprCompletionList = { reprPrec := Lapis.Protocol.Messages.instReprCompletionList.repr }

def Lapis.Protocol.Messages.instReprCompletionList.repr : CompletionList → Nat → Std.Format

Equations

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

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

Equations

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

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

• includeDeclaration : Bool

instance Lapis.Protocol.Messages.instInhabitedReferenceContext : Inhabited ReferenceContext

Equations

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

def Lapis.Protocol.Messages.instInhabitedReferenceContext.default : ReferenceContext

Equations

• Lapis.Protocol.Messages.instInhabitedReferenceContext.default = { includeDeclaration := default }

instance Lapis.Protocol.Messages.instReprReferenceContext : Repr ReferenceContext

Equations

• Lapis.Protocol.Messages.instReprReferenceContext = { reprPrec := Lapis.Protocol.Messages.instReprReferenceContext.repr }

def Lapis.Protocol.Messages.instReprReferenceContext.repr : ReferenceContext → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instToJsonReferenceContext : Lean.ToJson ReferenceContext

Equations

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

instance Lapis.Protocol.Messages.instFromJsonReferenceContext : Lean.FromJson ReferenceContext

Equations

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

structure Lapis.Protocol.Messages.ReferenceParams : Type

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

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

Equations

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

instance Lapis.Protocol.Messages.instInhabitedReferenceParams : Inhabited ReferenceParams

Equations

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

def Lapis.Protocol.Messages.instReprReferenceParams.repr : ReferenceParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprReferenceParams : Repr ReferenceParams

Equations

• Lapis.Protocol.Messages.instReprReferenceParams = { reprPrec := Lapis.Protocol.Messages.instReprReferenceParams.repr }

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

Equations

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

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

Workspace configuration item

• scopeUri : Option Types.DocumentUri
• section : Option String

instance Lapis.Protocol.Messages.instInhabitedConfigurationItem : Inhabited ConfigurationItem

Equations

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

def Lapis.Protocol.Messages.instInhabitedConfigurationItem.default : ConfigurationItem

Equations

• Lapis.Protocol.Messages.instInhabitedConfigurationItem.default = { scopeUri := default, «section» := default }

def Lapis.Protocol.Messages.instReprConfigurationItem.repr : ConfigurationItem → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprConfigurationItem : Repr ConfigurationItem

Equations

• Lapis.Protocol.Messages.instReprConfigurationItem = { reprPrec := Lapis.Protocol.Messages.instReprConfigurationItem.repr }

instance Lapis.Protocol.Messages.instToJsonConfigurationItem : Lean.ToJson ConfigurationItem

Equations

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

instance Lapis.Protocol.Messages.instFromJsonConfigurationItem : Lean.FromJson ConfigurationItem

Equations

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

structure Lapis.Protocol.Messages.ConfigurationParams : Type

Parameters for workspace/configuration request

• items : Array ConfigurationItem

def Lapis.Protocol.Messages.instInhabitedConfigurationParams.default : ConfigurationParams

Equations

• Lapis.Protocol.Messages.instInhabitedConfigurationParams.default = { items := default }

instance Lapis.Protocol.Messages.instInhabitedConfigurationParams : Inhabited ConfigurationParams

Equations

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

def Lapis.Protocol.Messages.instReprConfigurationParams.repr : ConfigurationParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Messages.instReprConfigurationParams : Repr ConfigurationParams

Equations

• Lapis.Protocol.Messages.instReprConfigurationParams = { reprPrec := Lapis.Protocol.Messages.instReprConfigurationParams.repr }

instance Lapis.Protocol.Messages.instToJsonConfigurationParams : Lean.ToJson ConfigurationParams

Equations

• Lapis.Protocol.Messages.instToJsonConfigurationParams = { toJson := fun (p : Lapis.Protocol.Messages.ConfigurationParams) => Lean.Json.mkObj [("items", Lean.toJson p.items)] }

instance Lapis.Protocol.Messages.instFromJsonConfigurationParams : Lean.FromJson ConfigurationParams

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

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.

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.