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
            instance instToJsonShowMessageParams :
            Lean.ToJson ShowMessageParams
            Equations
              source
              structure MessageActionItem :
              Type
              Instances For
                source
                instance instFromJsonMessageActionItem :
                Lean.FromJson MessageActionItem
                Equations
                  source
                  instance instToJsonMessageActionItem :
                  Lean.ToJson MessageActionItem
                  Equations
                    source
                    structure ShowMessageRequestParams :
                    Type
                    Instances For
                      source
                      instance instFromJsonShowMessageRequestParams :
                      Lean.FromJson ShowMessageRequestParams
                      Equations
                        source
                        instance instToJsonShowMessageRequestParams :
                        Lean.ToJson ShowMessageRequestParams
                        Equations
                          source
                          def ShowMessageResponse :
                          Type
                          Equations
                            Instances For
                              source
                              instance instShowMessageResponseFromJson :
                              Lean.FromJson ShowMessageResponse
                              Equations
                                source
                                instance instShowMessageResponseToJson :
                                Lean.ToJson ShowMessageResponse
                                Equations