package coq-aac-tactics

  1. Overview
  2. No Docs
AAC tactics

Install

Dune Dependency

github.com Edit opam file Versions (21)

Authors

  1. D
    Damien Pous <damien.pous@inria.fr>
  2. T
    Thomas Braibant <thomas.braibant@gmail.com>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=7686e0d53a2f619a51ad4ae73cafe8c6

Description

This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators:

Tags

keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure category:Miscellaneous/Coq Extensions

Published: 16 Apr 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6" & != "8.5.0~camlp4" & != "8.5.2~camlp4"
  2. ocaml

Dev Dependencies

None

Conflicts

None