Skip to content

arthuraa/coq-utils

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 

Coq Utils: a handful of useful Coq libraries

This package contains miscellaneous useful Coq libraries:

  • nominal: a simple theory of nominal sets with computable support, including the formalization of name restriction and binding operators.

  • word: theory of finite bit vectors.

  • hseq: heterogeneous lists.

  • string: basic infrastructure for some types in the Coq standard library.

The development is based on the SSReflect proof language and on the Mathematical Components libraries, and tries to follow their conventions and philosophy (for example, the use of canonical structures to define types with structure).

Installation

The package currently needs to be compiled by hand. The requirements are:

  • Coq v8.10 -- v8.13
  • coq-mathcomp-ssreflect, coq-mathcomp-fingroup, coq-mathcomp-algebra v1.11 -- v1.12
  • coq-deriving (v0.1)
  • coq-extructures (v0.3)

To compile the package, simply run

make

After compilation, you can install the package by running

make install

Usage

Documentation for the libraries is currently scarce, but will be progressively added as comments in the headers of the files. Once the package is installed, it can be required using the CoqUtils qualifier. For example:

From CoqUtils Require Import hseq nominal.

About

Some basic libraries for Coq.

Resources

License

Stars

Watchers

Forks

Packages

No packages published