| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | |||
| 3 | |||
| 4 | * Deal with implications | ||
| 5 | * Validate identifiers and locate conflicts | ||
| 6 | * Saving of proofs | ||
| 7 | * Relators | ||
| 8 | * Free-theorems | ||
| 9 | * Help menu | ||
| 10 | * Documentation (Haddock and manual) | ||
| 11 | * Tests | ||
| 12 | |||
| 13 | |||
| 14 | * Remove many (once ...) (very poor definition) | ||
| 15 | |||
| 16 | |||
| 17 | * Type equality in type annotations | ||
| 18 | * Type equality in safe cast of DEF | ||
| 19 | |||
| 20 | |||
| 21 | * Algebraic manipulation of rewriting strategies in order to simplify them and | ||
| 22 | identify possible non-termination situations. | ||
| 23 | * Automatically classify the rules according with the multiplicity of symbols. | ||
| 24 | * Proof steps seen as relations and thus proofs can be rewriten and simplified. | ||
| 25 |