package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Protect.ErrorSource

This module reifies Coq side effects into an algebraic structure.

This is very convenient for upper layer programming.

As of today we handle feedback, exceptions, and interruptions.

Sourcetype 'l t = private
  1. | User of 'l Message.Payload.t
  2. | Anomaly of 'l Message.Payload.t