package coq-aac-tactics

  1. Overview
  2. No Docs
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators

Install

Dune Dependency

github.com Edit opam file Versions (21)

Authors

  1. T
    Thomas Braibant
  2. D
    Damien Pous
  3. F
    Fabian Kunze

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.9.0.tar.gz
sha256=b4e124ccb2c0a9013af9d3dae6a0deb1962d224b36b64c11ec71c05c23fd2ea6

Description

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.

Tags

category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2019-05-16

Published: 16 May 2019

Dependencies (2)

  1. coq >= "8.9" & < "8.10~"
  2. ocaml

Dev Dependencies

None

Conflicts

None