tactics.md 806 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
# List of Tactics

In effort to make it easier for new users to get started with the RT-PROOFs project, this file maintains a list of the tactics used in the project.

Each tactic should be named and briefly described (just a few sentences). Please add links to additional documentation elsewhere (if available).

## Tactics from VBase

Tactics taken from the standard library of Viktor Vafeiadis.

- `des`: breaks all conjunctions in the local context, applies any simple substitutions via `subst`, and breaks any disjunctions in the local context into separate cases that are to be proved individually as subgoals.

*To be continued… please help out.*

## Tactics from `ssreflect`

*To be written… please feel free to start.*

## Standard Coq Tactics

*To be written… please feel free to start.*