 | 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 | > |
| abandon | Ivor.TT |
| addArg | Ivor.TT |
| addAxiom | Ivor.TT |
| addBinFn | Ivor.TT |
| addBinOp | Ivor.TT |
| addCommand | Ivor.Shell |
| addData | Ivor.TT |
| addDataNoElim | Ivor.TT |
| addDef | Ivor.TT |
| addEquality | Ivor.TT |
| addExternalFn | Ivor.TT |
| addGenRec | Ivor.TT |
| addImplicit | Ivor.TT |
| addModulePath | Ivor.Shell |
| addPatternDef | Ivor.TT |
| addPrimFn | Ivor.TT |
| addPrimitive | Ivor.TT |
| addPrimitives | Ivor.Primitives |
| addStdlibPath | Ivor.Shell |
| addTactic | Ivor.Shell |
| addTypedDef | Ivor.TT |
| allSolved | Ivor.TT |
| Annot | Ivor.ViewTerm, Ivor.TT |
| Annotation | Ivor.ViewTerm, Ivor.TT |
| annotation | Ivor.ViewTerm, Ivor.TT |
| App | Ivor.ViewTerm, Ivor.TT |
| apply | Ivor.ViewTerm, Ivor.TT |
| arg | Ivor.ViewTerm, Ivor.TT |
| arguments | Ivor.TT |
| attack | Ivor.TT |
| attackWith | Ivor.TT |
| auto | Ivor.Construction |
| axiomatise | Ivor.TT |