Documentation

Lean.Data.Lsp.Client

source
structure Lean.Lsp.Registration :
Type
Instances For
    source
    instance Lean.Lsp.instToJsonRegistration :
    ToJson Registration
    Equations
      source
      instance Lean.Lsp.instFromJsonRegistration :
      FromJson Registration
      Equations
        source
        structure Lean.Lsp.RegistrationParams :
        Type
        Instances For
          source
          instance Lean.Lsp.instToJsonRegistrationParams :
          ToJson RegistrationParams
          Equations
            source
            instance Lean.Lsp.instFromJsonRegistrationParams :
            FromJson RegistrationParams
            Equations