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. P
    palmskog@gmail.com

Sources

v8.6.1.tar.gz
md5=2d5a77e26ae85f1fb6ab0e5034787d45

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: 21 May 2017

Dependencies (2)

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

Dev Dependencies

None

Conflicts

None