agdarsec - Total Parser Combinators in Agda

The motivation and design decisions behind agdarsec are detailed in:

• this paper for the core design
• this blog post for the instrumentation

Compilation

To typecheck and compile this project you will need:

• Agda version 2.6.4.3
• Agda's standard library (version 2.0)

Ports

I have ported this library to other dependently-typed languages:

• parseque is the port to Coq
• and idris-tparsec the one for Idris