Documentation

Lean.Data.Lsp.Window

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