Library AAC_tactics.AAC
- Theory file for the aac_rewrite tactic
- Environments for the reification process: we use positive maps to index elements
- Classes for properties of operators
- Utilities for the evaluation function
- Utilities for positive numbers
- Dependent types utilities
- Utilities about (non-empty) lists and multisets
- Packaging structures
- Reification, normalisation, and decision
- Lemmas for performing transitivity steps
Library AAC_tactics.Instances
Library AAC_tactics.Tutorial
Library AAC_tactics.Caveats
- Currently known caveats and limitations of the aac_tactics library.
- Limitations
- Caveats
- 1. Special treatment for units.
- 2. Existential variables.
- 3. Distinction between aac_rewrite and aacu_rewrite
- 4. Rewriting units
- 5. Rewriting too much things.
- 6. Rewriting nullifiable patterns.
- Another example of the former case is the following, where the hypothesis can be instanciated to be equal to 1