Documentation

Lean.Data.Lsp.LanguageFeatures

Instances For
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        structure Lean.Lsp.Hover :
        Instances For
          • includeDeclaration : Bool
          Instances For
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • Lean.Lsp.instFromJsonDocumentSymbolAux = { fromJson? := Lean.Lsp.fromJsonDocumentSymbolAux✝ }
                Equations
                • Lean.Lsp.instToJsonDocumentSymbolAux = { toJson := Lean.Lsp.toJsonDocumentSymbolAux✝ }
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • tokenType.toNat = tokenType.toCtorIdx
                      Instances For

                        The semantic token modifiers included by default in the LSP specification. Not used by the Lean core, but implementing them here allows them to be utilized by users extending the Lean server.

                        Instances For
                          Equations
                          Instances For
                            Equations
                            • modifier.toNat = modifier.toCtorIdx
                            Instances For
                              Instances For
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    • prepareProvider : Bool
                                    Instances For