alectryon

Homepage: https://github.com/cpitclaudel/alectryon

Author: Clément Pit-Claudel

Updated: 2025-Jun-28

Summary

Toggle between Coq and reStructuredText

Commentary

This package is a thin wrapper around Alectryon's editor support
(https://github.com/cpitclaudel/alectryon).  The idea is to easily switch
between a code-first and a text-first view of a literate file.

Concretely, Alectryon converts back and forth between this:

    =============================
     Writing decision procedures
    =============================

    Here's an inductive type:

    .. coq::

       Inductive Even : nat -> Prop :=
       | EvenO : Even O
       | EvenS : forall n, Even n -> Even (S (S n)).

    .. note::

       It has two constructors:

       .. coq:: unfold out

          Check EvenO.
          Check EvenS.

… and this:

    (*|
    =============================
     Writing decision procedures
    =============================

    Here's an inductive type:
    |*)

    Inductive Even : nat -> Prop :=
    | EvenO : Even O
    | EvenS : forall n, Even n -> Even (S (S n)).

    (*|
    .. note::

       It has two constructors:

       .. coq:: unfold out
    |*)

    Check EvenO.
    Check EvenS.

Dependencies

• flycheck
• proof-general