Project Website Index Table of Contents
  • Utility functions and results for AAC Tactics
    • Utilities for positive numbers
    • Dependent types utilities
    • Utilities about (non-empty) lists and multisets
  • Theory for AAC Tactics
    • Environments for the reification process
    • Classes for properties of operators
    • Utilities for the evaluation function
    • Packaging structures
      • Free symbols
      • Binary operations
    • Reification, normalisation, and decision
      • Almost normalised syntax
      • Evaluation from syntax to the abstract domain
      • Normalisation
      • Correctness
    • Lemmas for performing transitivity steps given an AAC_lift instance
  • Instances for AAC Tactics
    • Peano instances
    • Z instances
    • List instances
    • N instances
    • Positive instances
    • Q instances
    • Prop instances
    • Boolean instances
    • Relation instances
  • Tutorial for using AAC Tactics
    • Introductory example
    • Usage
      • Selecting what and where to rewrite
      • Distinction between aac_rewrite and aacu_rewrite
      • Declaring instances
      • Working with inequations
      • Normalising goals
    • Examples from previous website
      • Reverse triangle inequality
      • Pythagorean triples
    • List examples
    • Prop examples
  • Currently known limitations and caveats of AAC Tactics
    • Limitations
      • Dependent parameters
      • Exogeneous morphisms
      • Treatment of variance with inequations
    • Caveats
      • Special treatment for units
      • Existential variables
      • Distinction between aac_rewrite and aacu_rewrite
      • Rewriting units
      • Rewriting too many things
      • Rewriting nullifiable patterns
      • If the pattern is a unit or can be instantiated to be equal to a unit
      • Another example of the former case
Generated by coqdoc and improved with CoqdocJS as adapted for coq-community