@[reducible, inline]

abbrev Lapis.Protocol.Types.DocumentUri : Type

Equations

• Lapis.Protocol.Types.DocumentUri = String

@[reducible, inline]

abbrev Lapis.Protocol.Types.Position : Type

Equations

• Lapis.Protocol.Types.Position = Lapis.Protocol.Generated.Position

@[reducible, inline]

abbrev Lapis.Protocol.Types.Range : Type

Equations

• Lapis.Protocol.Types.Range = Lapis.Protocol.Generated.Range

@[reducible, inline]

abbrev Lapis.Protocol.Types.Location : Type

Equations

• Lapis.Protocol.Types.Location = Lapis.Protocol.Generated.Location

@[reducible, inline]

abbrev Lapis.Protocol.Types.LocationLink : Type

Equations

• Lapis.Protocol.Types.LocationLink = Lapis.Protocol.Generated.LocationLink

@[reducible, inline]

abbrev Lapis.Protocol.Types.TextDocumentIdentifier : Type

Equations

• Lapis.Protocol.Types.TextDocumentIdentifier = Lapis.Protocol.Generated.TextDocumentIdentifier

@[reducible, inline]

abbrev Lapis.Protocol.Types.VersionedTextDocumentIdentifier : Type

Equations

• Lapis.Protocol.Types.VersionedTextDocumentIdentifier = Lapis.Protocol.Generated.VersionedTextDocumentIdentifier

structure Lapis.Protocol.Types.TextDocumentItem : Type

• uri : DocumentUri
• languageId : String
• version : Int
• text : String

@[implicit_reducible]

instance Lapis.Protocol.Types.instInhabitedTextDocumentItem : Inhabited TextDocumentItem

Equations

• Lapis.Protocol.Types.instInhabitedTextDocumentItem = { default := Lapis.Protocol.Types.instInhabitedTextDocumentItem.default }

def Lapis.Protocol.Types.instInhabitedTextDocumentItem.default : TextDocumentItem

Equations

• Lapis.Protocol.Types.instInhabitedTextDocumentItem.default = { uri := default, languageId := default, version := default, text := default }

@[implicit_reducible]

instance Lapis.Protocol.Types.instToJsonTextDocumentItem : Lean.ToJson TextDocumentItem

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Types.instFromJsonTextDocumentItem : Lean.FromJson TextDocumentItem

Equations

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

@[reducible, inline]

abbrev Lapis.Protocol.Types.TextDocumentPositionParams : Type

Equations

• Lapis.Protocol.Types.TextDocumentPositionParams = Lapis.Protocol.Generated.TextDocumentPositionParams

@[reducible, inline]

abbrev Lapis.Protocol.Types.TextEdit : Type

Equations

• Lapis.Protocol.Types.TextEdit = Lapis.Protocol.Generated.TextEdit

@[reducible, inline]

abbrev Lapis.Protocol.Types.DiagnosticSeverity : Type

Equations

• Lapis.Protocol.Types.DiagnosticSeverity = Lapis.Protocol.Generated.DiagnosticSeverity

@[reducible, inline]

abbrev Lapis.Protocol.Types.DiagnosticTag : Type

Equations

• Lapis.Protocol.Types.DiagnosticTag = Lapis.Protocol.Generated.DiagnosticTag

@[reducible, inline]

abbrev Lapis.Protocol.Types.DiagnosticRelatedInformation : Type

Equations

• Lapis.Protocol.Types.DiagnosticRelatedInformation = Lapis.Protocol.Generated.DiagnosticRelatedInformation

@[reducible, inline]

abbrev Lapis.Protocol.Types.MarkupKind : Type

Equations

• Lapis.Protocol.Types.MarkupKind = Lapis.Protocol.Generated.MarkupKind

@[reducible, inline]

abbrev Lapis.Protocol.Types.MarkupContent : Type

Equations

• Lapis.Protocol.Types.MarkupContent = Lapis.Protocol.Generated.MarkupContent

@[implicit_reducible]

instance Lapis.Protocol.Types.instOrdPosition : Ord Position

Equations

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

structure Lapis.Protocol.Types.Diagnostic : Type

• range : Range
• severity : Option DiagnosticSeverity
• code : Option String
• source : Option String
• message : String
• tags : Option (Array DiagnosticTag)
• relatedInformation : Option (Array DiagnosticRelatedInformation)

@[implicit_reducible]

instance Lapis.Protocol.Types.instInhabitedDiagnostic : Inhabited Diagnostic

Equations

• Lapis.Protocol.Types.instInhabitedDiagnostic = { default := Lapis.Protocol.Types.instInhabitedDiagnostic.default }

def Lapis.Protocol.Types.instInhabitedDiagnostic.default : Diagnostic

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Types.instToJsonDiagnostic : Lean.ToJson Diagnostic

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Types.instFromJsonDiagnostic : Lean.FromJson Diagnostic

Equations

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

structure Lapis.Protocol.Types.WorkDoneProgressParams : Type

• workDoneToken : Option String

@[implicit_reducible]

instance Lapis.Protocol.Types.instInhabitedWorkDoneProgressParams : Inhabited WorkDoneProgressParams

Equations

• Lapis.Protocol.Types.instInhabitedWorkDoneProgressParams = { default := Lapis.Protocol.Types.instInhabitedWorkDoneProgressParams.default }

def Lapis.Protocol.Types.instInhabitedWorkDoneProgressParams.default : WorkDoneProgressParams

Equations

• Lapis.Protocol.Types.instInhabitedWorkDoneProgressParams.default = { workDoneToken := default }

@[implicit_reducible]

instance Lapis.Protocol.Types.instReprWorkDoneProgressParams : Repr WorkDoneProgressParams

Equations

• Lapis.Protocol.Types.instReprWorkDoneProgressParams = { reprPrec := Lapis.Protocol.Types.instReprWorkDoneProgressParams.repr }

def Lapis.Protocol.Types.instReprWorkDoneProgressParams.repr : WorkDoneProgressParams → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Types.instToJsonWorkDoneProgressParams : Lean.ToJson WorkDoneProgressParams

Equations

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

@[implicit_reducible]

instance Lapis.Protocol.Types.instFromJsonWorkDoneProgressParams : Lean.FromJson WorkDoneProgressParams

Equations

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