package coq-lsp

  1. Overview
  2. Docs

This modules reifies Coq side effects into an algebraic structure.

This is obviously very convenient for upper layer programming.

As of today this includes feedback and exceptions.

type 'l payload = 'l option * Pp.t
type 'l t = private
  1. | User of 'l payload
  2. | Anomaly of 'l payload