@[reducible, inline]

abbrev Lapis.Protocol.Types.DocumentUri : Type

Equations

• Lapis.Protocol.Types.DocumentUri = String

structure Lapis.Protocol.Types.Position : Type

Position in a text document expressed as zero-based line and character offset

• line : Nat

  Line position in a document (zero-based).

• character : Nat

  Character offset on a line in a document (zero-based).

instance Lapis.Protocol.Types.instInhabitedPosition : Inhabited Position

Equations

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

def Lapis.Protocol.Types.instInhabitedPosition.default : Position

Equations

• Lapis.Protocol.Types.instInhabitedPosition.default = { line := default, character := default }

def Lapis.Protocol.Types.instBEqPosition.beq : Position → Position → Bool

Equations

• Lapis.Protocol.Types.instBEqPosition.beq { line := a, character := a_1 } { line := b, character := b_1 } = (a == b && a_1 == b_1)
• Lapis.Protocol.Types.instBEqPosition.beq x✝¹ x✝ = false

instance Lapis.Protocol.Types.instBEqPosition : BEq Position

Equations

• Lapis.Protocol.Types.instBEqPosition = { beq := Lapis.Protocol.Types.instBEqPosition.beq }

instance Lapis.Protocol.Types.instReprPosition : Repr Position

Equations

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

def Lapis.Protocol.Types.instReprPosition.repr : Position → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonPosition : Lean.ToJson Position

Equations

• Lapis.Protocol.Types.instToJsonPosition = { toJson := fun (p : Lapis.Protocol.Types.Position) => Lean.Json.mkObj [("line", Lean.toJson p.line), ("character", Lean.toJson p.character)] }

instance Lapis.Protocol.Types.instFromJsonPosition : Lean.FromJson Position

Equations

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

instance Lapis.Protocol.Types.instOrdPosition : Ord Position

Equations

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

structure Lapis.Protocol.Types.Range : Type

A range in a text document expressed as (zero-based) start and end positions

• start : Position

  The range's start position

• end : Position

  The range's end position

instance Lapis.Protocol.Types.instInhabitedRange : Inhabited Range

Equations

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

def Lapis.Protocol.Types.instInhabitedRange.default : Range

Equations

• Lapis.Protocol.Types.instInhabitedRange.default = { start := default, «end» := default }

instance Lapis.Protocol.Types.instBEqRange : BEq Range

Equations

• Lapis.Protocol.Types.instBEqRange = { beq := Lapis.Protocol.Types.instBEqRange.beq }

def Lapis.Protocol.Types.instBEqRange.beq : Range → Range → Bool

Equations

• Lapis.Protocol.Types.instBEqRange.beq { start := a, «end» := a_1 } { start := b, «end» := b_1 } = (a == b && a_1 == b_1)
• Lapis.Protocol.Types.instBEqRange.beq x✝¹ x✝ = false

instance Lapis.Protocol.Types.instReprRange : Repr Range

Equations

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

def Lapis.Protocol.Types.instReprRange.repr : Range → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonRange : Lean.ToJson Range

Equations

• Lapis.Protocol.Types.instToJsonRange = { toJson := fun (r : Lapis.Protocol.Types.Range) => Lean.Json.mkObj [("start", Lean.toJson r.start), ("end", Lean.toJson r.end)] }

instance Lapis.Protocol.Types.instFromJsonRange : Lean.FromJson Range

Equations

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

structure Lapis.Protocol.Types.Location : Type

A location inside a resource, such as a line inside a text file

• uri : DocumentUri

  The document URI

• range : Range

  The range within the document

def Lapis.Protocol.Types.instInhabitedLocation.default : Location

Equations

• Lapis.Protocol.Types.instInhabitedLocation.default = { uri := default, range := default }

instance Lapis.Protocol.Types.instInhabitedLocation : Inhabited Location

Equations

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

def Lapis.Protocol.Types.instBEqLocation.beq : Location → Location → Bool

Equations

• Lapis.Protocol.Types.instBEqLocation.beq { uri := a, range := a_1 } { uri := b, range := b_1 } = (a == b && a_1 == b_1)
• Lapis.Protocol.Types.instBEqLocation.beq x✝¹ x✝ = false

instance Lapis.Protocol.Types.instBEqLocation : BEq Location

Equations

• Lapis.Protocol.Types.instBEqLocation = { beq := Lapis.Protocol.Types.instBEqLocation.beq }

def Lapis.Protocol.Types.instReprLocation.repr : Location → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instReprLocation : Repr Location

Equations

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

instance Lapis.Protocol.Types.instToJsonLocation : Lean.ToJson Location

Equations

• Lapis.Protocol.Types.instToJsonLocation = { toJson := fun (l : Lapis.Protocol.Types.Location) => Lean.Json.mkObj [("uri", Lean.toJson l.uri), ("range", Lean.toJson l.range)] }

instance Lapis.Protocol.Types.instFromJsonLocation : Lean.FromJson Location

Equations

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

structure Lapis.Protocol.Types.LocationLink : Type

• originSelectionRange : Option Range
• targetUri : DocumentUri
• targetRange : Range
• targetSelectionRange : Range

instance Lapis.Protocol.Types.instInhabitedLocationLink : Inhabited LocationLink

Equations

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

def Lapis.Protocol.Types.instInhabitedLocationLink.default : LocationLink

Equations

• Lapis.Protocol.Types.instInhabitedLocationLink.default = { originSelectionRange := default, targetUri := default, targetRange := default, targetSelectionRange := default }

instance Lapis.Protocol.Types.instBEqLocationLink : BEq LocationLink

Equations

• Lapis.Protocol.Types.instBEqLocationLink = { beq := Lapis.Protocol.Types.instBEqLocationLink.beq }

def Lapis.Protocol.Types.instBEqLocationLink.beq : LocationLink → LocationLink → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lapis.Protocol.Types.instBEqLocationLink.beq x✝¹ x✝ = false

def Lapis.Protocol.Types.instReprLocationLink.repr : LocationLink → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instReprLocationLink : Repr LocationLink

Equations

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

instance Lapis.Protocol.Types.instToJsonLocationLink : Lean.ToJson LocationLink

Equations

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

instance Lapis.Protocol.Types.instFromJsonLocationLink : Lean.FromJson LocationLink

Equations

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

structure Lapis.Protocol.Types.TextDocumentIdentifier : Type

• uri : DocumentUri

instance Lapis.Protocol.Types.instInhabitedTextDocumentIdentifier : Inhabited TextDocumentIdentifier

Equations

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

def Lapis.Protocol.Types.instInhabitedTextDocumentIdentifier.default : TextDocumentIdentifier

Equations

• Lapis.Protocol.Types.instInhabitedTextDocumentIdentifier.default = { uri := default }

def Lapis.Protocol.Types.instBEqTextDocumentIdentifier.beq : TextDocumentIdentifier → TextDocumentIdentifier → Bool

Equations

• Lapis.Protocol.Types.instBEqTextDocumentIdentifier.beq { uri := a } { uri := b } = (a == b)
• Lapis.Protocol.Types.instBEqTextDocumentIdentifier.beq x✝¹ x✝ = false

instance Lapis.Protocol.Types.instBEqTextDocumentIdentifier : BEq TextDocumentIdentifier

Equations

• Lapis.Protocol.Types.instBEqTextDocumentIdentifier = { beq := Lapis.Protocol.Types.instBEqTextDocumentIdentifier.beq }

instance Lapis.Protocol.Types.instReprTextDocumentIdentifier : Repr TextDocumentIdentifier

Equations

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

def Lapis.Protocol.Types.instReprTextDocumentIdentifier.repr : TextDocumentIdentifier → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonTextDocumentIdentifier : Lean.ToJson TextDocumentIdentifier

Equations

• Lapis.Protocol.Types.instToJsonTextDocumentIdentifier = { toJson := fun (t : Lapis.Protocol.Types.TextDocumentIdentifier) => Lean.Json.mkObj [("uri", Lean.toJson t.uri)] }

instance Lapis.Protocol.Types.instFromJsonTextDocumentIdentifier : Lean.FromJson TextDocumentIdentifier

Equations

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

structure Lapis.Protocol.Types.VersionedTextDocumentIdentifier : Type

• uri : DocumentUri
• version : Int

def Lapis.Protocol.Types.instInhabitedVersionedTextDocumentIdentifier.default : VersionedTextDocumentIdentifier

Equations

• Lapis.Protocol.Types.instInhabitedVersionedTextDocumentIdentifier.default = { uri := default, version := default }

instance Lapis.Protocol.Types.instInhabitedVersionedTextDocumentIdentifier : Inhabited VersionedTextDocumentIdentifier

Equations

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

def Lapis.Protocol.Types.instBEqVersionedTextDocumentIdentifier.beq : VersionedTextDocumentIdentifier → VersionedTextDocumentIdentifier → Bool

Equations

• Lapis.Protocol.Types.instBEqVersionedTextDocumentIdentifier.beq { uri := a, version := a_1 } { uri := b, version := b_1 } = (a == b && a_1 == b_1)
• Lapis.Protocol.Types.instBEqVersionedTextDocumentIdentifier.beq x✝¹ x✝ = false

instance Lapis.Protocol.Types.instBEqVersionedTextDocumentIdentifier : BEq VersionedTextDocumentIdentifier

Equations

• Lapis.Protocol.Types.instBEqVersionedTextDocumentIdentifier = { beq := Lapis.Protocol.Types.instBEqVersionedTextDocumentIdentifier.beq }

instance Lapis.Protocol.Types.instReprVersionedTextDocumentIdentifier : Repr VersionedTextDocumentIdentifier

Equations

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

def Lapis.Protocol.Types.instReprVersionedTextDocumentIdentifier.repr : VersionedTextDocumentIdentifier → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonVersionedTextDocumentIdentifier : Lean.ToJson VersionedTextDocumentIdentifier

Equations

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

instance Lapis.Protocol.Types.instFromJsonVersionedTextDocumentIdentifier : Lean.FromJson VersionedTextDocumentIdentifier

Equations

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

structure Lapis.Protocol.Types.TextDocumentItem : Type

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

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

Equations

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

instance Lapis.Protocol.Types.instInhabitedTextDocumentItem : Inhabited TextDocumentItem

Equations

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

instance Lapis.Protocol.Types.instReprTextDocumentItem : Repr TextDocumentItem

Equations

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

def Lapis.Protocol.Types.instReprTextDocumentItem.repr : TextDocumentItem → Nat → Std.Format

Equations

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

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

Equations

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

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

Equations

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

structure Lapis.Protocol.Types.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lapis.Protocol.Types.instInhabitedTextDocumentPositionParams : Inhabited TextDocumentPositionParams

Equations

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

def Lapis.Protocol.Types.instInhabitedTextDocumentPositionParams.default : TextDocumentPositionParams

Equations

• Lapis.Protocol.Types.instInhabitedTextDocumentPositionParams.default = { textDocument := default, position := default }

def Lapis.Protocol.Types.instReprTextDocumentPositionParams.repr : TextDocumentPositionParams → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instReprTextDocumentPositionParams : Repr TextDocumentPositionParams

Equations

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

instance Lapis.Protocol.Types.instToJsonTextDocumentPositionParams : Lean.ToJson TextDocumentPositionParams

Equations

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

instance Lapis.Protocol.Types.instFromJsonTextDocumentPositionParams : Lean.FromJson TextDocumentPositionParams

Equations

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

structure Lapis.Protocol.Types.TextEdit : Type

• range : Range
• newText : String

instance Lapis.Protocol.Types.instInhabitedTextEdit : Inhabited TextEdit

Equations

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

def Lapis.Protocol.Types.instInhabitedTextEdit.default : TextEdit

Equations

• Lapis.Protocol.Types.instInhabitedTextEdit.default = { range := default, newText := default }

instance Lapis.Protocol.Types.instReprTextEdit : Repr TextEdit

Equations

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

def Lapis.Protocol.Types.instReprTextEdit.repr : TextEdit → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonTextEdit : Lean.ToJson TextEdit

Equations

• Lapis.Protocol.Types.instToJsonTextEdit = { toJson := fun (e : Lapis.Protocol.Types.TextEdit) => Lean.Json.mkObj [("range", Lean.toJson e.range), ("newText", Lean.toJson e.newText)] }

instance Lapis.Protocol.Types.instFromJsonTextEdit : Lean.FromJson TextEdit

Equations

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

inductive Lapis.Protocol.Types.DiagnosticSeverity : Type

• error : DiagnosticSeverity
• warning : DiagnosticSeverity
• information : DiagnosticSeverity
• hint : DiagnosticSeverity

instance Lapis.Protocol.Types.instInhabitedDiagnosticSeverity : Inhabited DiagnosticSeverity

Equations

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

def Lapis.Protocol.Types.instInhabitedDiagnosticSeverity.default : DiagnosticSeverity

Equations

• Lapis.Protocol.Types.instInhabitedDiagnosticSeverity.default = Lapis.Protocol.Types.DiagnosticSeverity.error

def Lapis.Protocol.Types.instBEqDiagnosticSeverity.beq : DiagnosticSeverity → DiagnosticSeverity → Bool

Equations

• Lapis.Protocol.Types.instBEqDiagnosticSeverity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lapis.Protocol.Types.instBEqDiagnosticSeverity : BEq DiagnosticSeverity

Equations

• Lapis.Protocol.Types.instBEqDiagnosticSeverity = { beq := Lapis.Protocol.Types.instBEqDiagnosticSeverity.beq }

def Lapis.Protocol.Types.instReprDiagnosticSeverity.repr : DiagnosticSeverity → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instReprDiagnosticSeverity : Repr DiagnosticSeverity

Equations

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

instance Lapis.Protocol.Types.instToJsonDiagnosticSeverity : Lean.ToJson DiagnosticSeverity

Equations

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

instance Lapis.Protocol.Types.instFromJsonDiagnosticSeverity : Lean.FromJson DiagnosticSeverity

Equations

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

inductive Lapis.Protocol.Types.DiagnosticTag : Type

• unnecessary : DiagnosticTag
• deprecated : DiagnosticTag

instance Lapis.Protocol.Types.instInhabitedDiagnosticTag : Inhabited DiagnosticTag

Equations

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

def Lapis.Protocol.Types.instInhabitedDiagnosticTag.default : DiagnosticTag

Equations

• Lapis.Protocol.Types.instInhabitedDiagnosticTag.default = Lapis.Protocol.Types.DiagnosticTag.unnecessary

instance Lapis.Protocol.Types.instBEqDiagnosticTag : BEq DiagnosticTag

Equations

• Lapis.Protocol.Types.instBEqDiagnosticTag = { beq := Lapis.Protocol.Types.instBEqDiagnosticTag.beq }

def Lapis.Protocol.Types.instBEqDiagnosticTag.beq : DiagnosticTag → DiagnosticTag → Bool

Equations

• Lapis.Protocol.Types.instBEqDiagnosticTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lapis.Protocol.Types.instReprDiagnosticTag : Repr DiagnosticTag

Equations

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

def Lapis.Protocol.Types.instReprDiagnosticTag.repr : DiagnosticTag → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonDiagnosticTag : Lean.ToJson DiagnosticTag

Equations

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

instance Lapis.Protocol.Types.instFromJsonDiagnosticTag : Lean.FromJson DiagnosticTag

Equations

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

structure Lapis.Protocol.Types.DiagnosticRelatedInformation : Type

Diagnostic related information

• location : Location
• message : String

def Lapis.Protocol.Types.instInhabitedDiagnosticRelatedInformation.default : DiagnosticRelatedInformation

Equations

• Lapis.Protocol.Types.instInhabitedDiagnosticRelatedInformation.default = { location := default, message := default }

instance Lapis.Protocol.Types.instInhabitedDiagnosticRelatedInformation : Inhabited DiagnosticRelatedInformation

Equations

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

instance Lapis.Protocol.Types.instReprDiagnosticRelatedInformation : Repr DiagnosticRelatedInformation

Equations

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

def Lapis.Protocol.Types.instReprDiagnosticRelatedInformation.repr : DiagnosticRelatedInformation → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonDiagnosticRelatedInformation : Lean.ToJson DiagnosticRelatedInformation

Equations

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

instance Lapis.Protocol.Types.instFromJsonDiagnosticRelatedInformation : Lean.FromJson DiagnosticRelatedInformation

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)

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.

def Lapis.Protocol.Types.instReprDiagnostic.repr : Diagnostic → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instReprDiagnostic : Repr Diagnostic

Equations

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

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

Equations

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

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

Equations

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

inductive Lapis.Protocol.Types.MarkupKind : Type

• plaintext : MarkupKind
• markdown : MarkupKind

instance Lapis.Protocol.Types.instInhabitedMarkupKind : Inhabited MarkupKind

Equations

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

def Lapis.Protocol.Types.instInhabitedMarkupKind.default : MarkupKind

Equations

• Lapis.Protocol.Types.instInhabitedMarkupKind.default = Lapis.Protocol.Types.MarkupKind.plaintext

instance Lapis.Protocol.Types.instBEqMarkupKind : BEq MarkupKind

Equations

• Lapis.Protocol.Types.instBEqMarkupKind = { beq := Lapis.Protocol.Types.instBEqMarkupKind.beq }

def Lapis.Protocol.Types.instBEqMarkupKind.beq : MarkupKind → MarkupKind → Bool

Equations

• Lapis.Protocol.Types.instBEqMarkupKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lapis.Protocol.Types.instReprMarkupKind : Repr MarkupKind

Equations

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

def Lapis.Protocol.Types.instReprMarkupKind.repr : MarkupKind → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instToJsonMarkupKind : Lean.ToJson MarkupKind

Equations

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

instance Lapis.Protocol.Types.instFromJsonMarkupKind : Lean.FromJson MarkupKind

Equations

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

structure Lapis.Protocol.Types.MarkupContent : Type

• kind : MarkupKind
• value : String

def Lapis.Protocol.Types.instInhabitedMarkupContent.default : MarkupContent

Equations

• Lapis.Protocol.Types.instInhabitedMarkupContent.default = { kind := default, value := default }

instance Lapis.Protocol.Types.instInhabitedMarkupContent : Inhabited MarkupContent

Equations

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

def Lapis.Protocol.Types.instReprMarkupContent.repr : MarkupContent → Nat → Std.Format

Equations

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

instance Lapis.Protocol.Types.instReprMarkupContent : Repr MarkupContent

Equations

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

instance Lapis.Protocol.Types.instToJsonMarkupContent : Lean.ToJson MarkupContent

Equations

• Lapis.Protocol.Types.instToJsonMarkupContent = { toJson := fun (m : Lapis.Protocol.Types.MarkupContent) => Lean.Json.mkObj [("kind", Lean.toJson m.kind), ("value", Lean.toJson m.value)] }

instance Lapis.Protocol.Types.instFromJsonMarkupContent : Lean.FromJson MarkupContent

Equations

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

structure Lapis.Protocol.Types.WorkDoneProgressParams : Type

• workDoneToken : Option String

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

Equations

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

instance Lapis.Protocol.Types.instInhabitedWorkDoneProgressParams : Inhabited WorkDoneProgressParams

Equations

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

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

Equations

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

instance Lapis.Protocol.Types.instReprWorkDoneProgressParams : Repr WorkDoneProgressParams

Equations

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

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

Equations

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

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

Equations

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