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
-
https://github.com/coq-community/aac-tactics
License
- GPL-3.0-or-later
Maintainers
-
Siraphob Phipathananunth
Outputs
out
(expand/collapse)
- /lib/coq/8.13/user-contrib/AAC_tactics/AAC.glob
- /lib/coq/8.13/user-contrib/AAC_tactics/AAC.v
- /lib/coq/8.13/user-contrib/AAC_tactics/AAC.vo
- /lib/coq/8.13/user-contrib/AAC_tactics/Caveats.glob
- /lib/coq/8.13/user-contrib/AAC_tactics/Caveats.v
- /lib/coq/8.13/user-contrib/AAC_tactics/Caveats.vo
- /lib/coq/8.13/user-contrib/AAC_tactics/Constants.glob
- /lib/coq/8.13/user-contrib/AAC_tactics/Constants.v
- /lib/coq/8.13/user-contrib/AAC_tactics/Constants.vo
- /lib/coq/8.13/user-contrib/AAC_tactics/Instances.glob
- /lib/coq/8.13/user-contrib/AAC_tactics/Instances.v
- /lib/coq/8.13/user-contrib/AAC_tactics/Instances.vo
- /lib/coq/8.13/user-contrib/AAC_tactics/Tutorial.glob
- /lib/coq/8.13/user-contrib/AAC_tactics/Tutorial.v
- /lib/coq/8.13/user-contrib/AAC_tactics/Tutorial.vo
- /lib/coq/8.13/user-contrib/AAC_tactics/Utils.glob
- /lib/coq/8.13/user-contrib/AAC_tactics/Utils.v
- /lib/coq/8.13/user-contrib/AAC_tactics/Utils.vo
- /lib/coq/8.13/user-contrib/AAC_tactics/aac_plugin.cmi
- /lib/coq/8.13/user-contrib/AAC_tactics/aac_plugin.cmx
- /lib/coq/8.13/user-contrib/AAC_tactics/aac_plugin.cmxa
- /lib/coq/8.13/user-contrib/AAC_tactics/aac_plugin.cmxs
Releases
8.13.0
(expand/collapse)