This is a library of useful utility functions for Coq plugins. These functions originally come from PUMPKIN PATCH and DEVOID, but may be useful for plugin development more broadly.

To build this library with a test plugin, run:

./build.sh

See PUMPKIN PATCH and DEVOID for examples of loading it as a submodule.

Guide

• LICENSE: License
• README.md: You are here!
• build.sh: Build script for example plugin
• theories: Example plugin that loads the library
• src: Main source directory
  • plib.mlpack
  • plibrary.ml4: Top-level file
  • utilities: General OCaml utilities
  • coq: Coq utilities
    • constants: Useful Coq constants, like sigma types and equality
    • devutils: Utilities for development, like printing terms with deBruijn indices
    • logicutils: Utilities for the core logic of Coq
      • contexts: Contexts, environments, and state for unification
      • hofs: Useful higher-order functions, like flexible reduction and substistution functions
      • inductive: Inductive types
      • transformation: Transforming types and terms
      • typesandequality: Type checking & inference, unification, convertibility, and so on
    • representationutils: Definitions, names, and dealing with different representations of terms
    • termutils: Utilities for constructing and reasoning about certain kinds of terms, like constants and functions

Contributors

This library was developed by Talia Ringer, Nate Yazdani, and RanDair Porter.

Licensing

We use the MIT license because we think Coq plugins have a right not to use GPL. If this is wrong, please let us know kindly so we can fix this.