blob: 7b7195def3cd107d8e0839c2a040e95c6d962f1d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Name: AACTactics
Title: AAC tactics
Description: This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators:
Keywords: reflexive tactic, rewriting, rewriting modulo associativity and commutativity, rewriting modulo AC, reflexive decision procedure
Category: Miscellaneous/Coq Extensions
Author: Thomas Braibant
Email: thomas.braibant@gmail.com
Homepage: http://sardes.inrialpes.fr/~braibant/
Institution: INRIA/UJF/Ens Lyon
Author: Damien Pous
Email: damien.pous@inria.fr
Homepage: http://sardes.inrialpes.fr/~pous/
Institution: CNRS
Require:
License: LGPL
|
