Documentation

Lean.Data.Lsp.Client

source
structure Lean.Lsp.Registration :
Type
Instances For
    source
    def Lean.Lsp.instToJsonRegistration.toJson :
    Registration → Json
    Equations
      Instances For
        source
        instance Lean.Lsp.instToJsonRegistration :
        ToJson Registration
        Equations
          source
          instance Lean.Lsp.instFromJsonRegistration :
          FromJson Registration
          Equations
            source
            def Lean.Lsp.instFromJsonRegistration.fromJson :
            Json → Except String Registration
            Equations
              Instances For
                source
                structure Lean.Lsp.RegistrationParams :
                Type
                Instances For
                  source
                  def Lean.Lsp.instToJsonRegistrationParams.toJson :
                  RegistrationParams → Json
                  Equations
                    Instances For
                      source
                      instance Lean.Lsp.instToJsonRegistrationParams :
                      ToJson RegistrationParams
                      Equations
                        source
                        def Lean.Lsp.instFromJsonRegistrationParams.fromJson :
                        Json → Except String RegistrationParams
                        Equations
                          Instances For
                            source
                            instance Lean.Lsp.instFromJsonRegistrationParams :
                            FromJson RegistrationParams
                            Equations