nixpkgs / coqPackages.aac-tactics - This Coq plugin provides tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator. The tactics can be applied for custom operators by registering the operators and their properties as type class instances. Many common operator instances, such as for Z binary arithmetic and booleans, are provided with the plugin.

Homepage -

License - GPL-3.0-or-later

Maintainers - Siraphob Phipathananunth


out (expand/collapse)


8.13.0 (expand/collapse)
From commit 0061117c to 00460bd6