Package: libaac-tactics-ocaml (8.8.0+1.gbp069dc3b-1 and others) [debports]
Links for libaac-tactics-ocaml
- Homepage [github.com]
Coq tactics for reasoning modulo AC (plugin)
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.
This package provides the plugin itself.
Other Packages Related to libaac-tactics-ocaml
- rec: libaac-tactics-coq
- Coq tactics for reasoning modulo AC (theories)
- enh: coq
- proof assistant for higher-order logic (toplevel and compiler)