Parseque

Port of the agdarsec total parser combinator library to Rocq/Coq.

Meta

• Author(s):
  • G. Allais (initial)
• Rocq-community maintainer(s):
  • Wolfgang Meier (@womeier)
• License: MIT License
• Compatible Rocq/Coq versions: 9.0 or later (for older versions see opam/nix)
• Additional dependencies: none
• Rocq/Coq namespace: parseque
• Related publication(s):
  • agdarsec - Total Parser Combinators

Building and installation instructions

The easiest way to install the latest released version of Parseque
is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-parseque

To instead build and install manually, do:

git clone https://github.com/rocq-community/parseque.git
cd parseque
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

This Rocq/Coq library is a port of the agdarsec
library for Agda. The core design of agdarsec is described in
this paper, while
this blog post
describes instrumentation.