Documentation

Lean.Data.Lsp.Window

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