This file contains types for communication between the watchdog and the workers. These messages are not visible externally to users of the LSP server.

Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON.

Instances For

    References from a single module/file

    Instances For

      $/lean/ileanInfoUpdate and $/lean/ileanInfoFinal watchdog<-worker notifications.

      Contains the file's definitions and references.

      Instances For