 | ivor-0.1.11: Theorem proving library based on dependent type theory | Contents | Index |
| A | B | C | D | E | F | G | H | I | K | L | M | N | O | P | Q | R | S | T | U | V | W | > |
| tacs | Ivor.TT |
| Tactic | Ivor.TT |
| Term | |
| 1 (Type/Class) | Ivor.ViewTerm, Ivor.TT |
| 2 (Data Constructor) | Ivor.ViewTerm, Ivor.TT |
| term | Ivor.ViewTerm, Ivor.TT |
| thaw | Ivor.TT |
| theorem | Ivor.TT |
| toPattern | Ivor.TT |
| traceTac | Ivor.TT |
| transform | Ivor.ViewTerm, Ivor.TT |
| trivial | Ivor.TT |
| try | Ivor.TT |
| trySolve | Ivor.TT |
| TTError | Ivor.TT |
| ttfail | Ivor.TT |
| TTM | Ivor.TT |
| TypeCon | Ivor.ViewTerm, Ivor.TT |
| typecon | Ivor.ViewTerm, Ivor.TT |
| typeof | Ivor.ViewTerm, Ivor.TT |