Convenience functions for unit testing in Coq.
Coq Shell
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
.gitignore
LICENSE
Make
README.md
configure.sh

README.md

Logo CUnit

Convenience functions for unit testing in Coq.

Require Import Coq.Lists.List.
Require Import CUnit.All.

Import ListNotations.

Definition test_plus : List.map_pair plus
  [(0, 0); (0, 3); (4, 0); (4, 3)] =
  [0; 3; 4; 7] :=
  eq_refl.

Install

With OPAM

Install the Coq repository:

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

and run:

opam install coq-cunit

From the sources

Run:

./configure.sh
make
make install

Reference

List

  • List.map_pair {A B C} (f : A -> B -> C) (l : list (A * B)) : list C
  • List.map_triple {A B C D} (f : A -> B -> C -> D) (l : list (A * B * C)) : list D
  • List.map_quad {A B C D E} (f : A -> B -> C -> D -> E) (l : list (A * B * C * D)) : list E