package coq-lsp

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Protect.ErrorSource

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.

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

Innovation. Community. Security.