Documentation

Lean.Data.Lsp.Window

source
inductive Lean.Lsp.MessageType :
Type
Instances For
    source
    @[instance_reducible]
    instance Lean.Lsp.instFromJsonMessageType :
    FromJson MessageType
    source
    @[instance_reducible]
    instance Lean.Lsp.instToJsonMessageType :
    ToJson MessageType
    source
    structure Lean.Lsp.ShowMessageParams :
    Type
    Instances For
      source
      @[instance_reducible]
      instance Lean.Lsp.instFromJsonShowMessageParams :
      FromJson ShowMessageParams
      source
      def Lean.Lsp.instFromJsonShowMessageParams.fromJson :
      Json → Except String ShowMessageParams
      Instances For
        source
        @[instance_reducible]
        instance Lean.Lsp.instToJsonShowMessageParams :
        ToJson ShowMessageParams
        source
        def Lean.Lsp.instToJsonShowMessageParams.toJson :
        ShowMessageParams → Json
        Instances For
          source
          structure Lean.Lsp.MessageActionItem :
          Type
          Instances For
            source
            def Lean.Lsp.instFromJsonMessageActionItem.fromJson :
            Json → Except String MessageActionItem
            Instances For
              source
              @[instance_reducible]
              instance Lean.Lsp.instFromJsonMessageActionItem :
              FromJson MessageActionItem
              source
              def Lean.Lsp.instToJsonMessageActionItem.toJson :
              MessageActionItem → Json
              Instances For
                source
                @[instance_reducible]
                instance Lean.Lsp.instToJsonMessageActionItem :
                ToJson MessageActionItem
                source
                structure Lean.Lsp.ShowMessageRequestParams :
                Type
                Instances For
                  source
                  @[instance_reducible]
                  instance Lean.Lsp.instFromJsonShowMessageRequestParams :
                  FromJson ShowMessageRequestParams
                  source
                  def Lean.Lsp.instFromJsonShowMessageRequestParams.fromJson :
                  Json → Except String ShowMessageRequestParams
                  Instances For
                    source
                    def Lean.Lsp.instToJsonShowMessageRequestParams.toJson :
                    ShowMessageRequestParams → Json
                    Instances For
                      source
                      @[instance_reducible]
                      instance Lean.Lsp.instToJsonShowMessageRequestParams :
                      ToJson ShowMessageRequestParams
                      source
                      def Lean.Lsp.ShowMessageResponse :
                      Type
                      Instances For
                        source
                        @[instance_reducible]
                        instance Lean.Lsp.instFromJsonShowMessageResponse :
                        FromJson ShowMessageResponse
                        source
                        @[instance_reducible]
                        instance Lean.Lsp.instToJsonShowMessageResponse :
                        ToJson ShowMessageResponse