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.1.tar.gz
md5=30bef1d940f0a13246318883bcc29baf

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: 18 Apr 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Conflicts

None