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.