Contribution: AACTactics

AAC tactics

Authors

• Thomas Braibant
• Damien Pous

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

Available files

• AAC_tactics.AAC.html
• AAC_tactics.Tutorial.html
• AAC_tactics.Instances.html
• AAC_tactics.Caveats.html