 | 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 | > |
| idTac | Ivor.TT |
| importFile | Ivor.Shell |
| indices | Ivor.ViewTerm, Ivor.TT |
| induction | Ivor.TT |
| Inductive | |
| 1 (Type/Class) | Ivor.ViewTerm, Ivor.TT |
| 2 (Data Constructor) | Ivor.ViewTerm, Ivor.TT |
| interactive | Ivor.TT |
| intro | Ivor.TT |
| introName | Ivor.TT |
| intros | Ivor.TT |
| intros1 | Ivor.TT |
| introsNames | Ivor.TT |
| isAuxPattern | Ivor.TT |
| IsData | Ivor.TT |
| isItJust | Ivor.Construction |
| IsTerm | Ivor.TT |