| >+> | Ivor.TT | | >-> | Ivor.TT | | >=> | Ivor.TT | | >|> | Ivor.TT | | 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 | | basicRefine | Ivor.TT | | beta | Ivor.TT | | bindings | Ivor.TT | | Bound | Ivor.ViewTerm, Ivor.TT | | by | Ivor.TT | | Call | Ivor.ViewTerm, Ivor.TT | | call | Ivor.TT | | callterm | Ivor.ViewTerm, Ivor.TT | | CantUnify | Ivor.TT | | Case | Ivor.TT | | cases | Ivor.TT | | check | Ivor.TT | | checkCtxt | Ivor.TT | | claim | Ivor.TT | | clearSaved | Ivor.TT | | Code | Ivor.ViewTerm, Ivor.TT | | codetype | Ivor.ViewTerm, Ivor.TT | | compile | Ivor.TT | | compute | Ivor.TT | | configureEq | Ivor.Shell | | Constant | Ivor.ViewTerm, Ivor.TT | | constructors | Ivor.ViewTerm, Ivor.TT | | Context | Ivor.TT | | contype | Ivor.ViewTerm, Ivor.TT | | converts | Ivor.TT | | DataCon | Ivor.ViewTerm, Ivor.TT | | dbgshow | Ivor.ViewTerm, Ivor.TT | | declare | Ivor.TT | | declareData | Ivor.TT | | defaultGoal | Ivor.TT | | defined | Ivor.TT | | dependentGeneralise | Ivor.TT | | displayName | Ivor.ViewTerm, Ivor.TT | | Elim | Ivor.TT | | ElimOp | Ivor.ViewTerm, Ivor.TT | | emptyContext | Ivor.TT | | equiv | Ivor.TT | | ErrContext | Ivor.TT | | Escape | Ivor.ViewTerm, Ivor.TT | | escapedterm | Ivor.ViewTerm, Ivor.TT | | Eval | Ivor.ViewTerm, Ivor.TT | | eval | Ivor.TT | | evalCtxt | Ivor.TT | | evalnew | Ivor.TT | | evalterm | Ivor.ViewTerm, Ivor.TT | | exists | Ivor.Construction | | extendParser | Ivor.Shell | | fargs | Ivor.ViewTerm, Ivor.TT | | fastCheck | Ivor.TT | | FileLoc | Ivor.ViewTerm, Ivor.TT | | fill | Ivor.TT | | fname | Ivor.ViewTerm, Ivor.TT | | focus | Ivor.TT | | Forall | Ivor.ViewTerm, Ivor.TT | | forgetDef | Ivor.TT | | Free | Ivor.ViewTerm, Ivor.TT | | freeIn | Ivor.ViewTerm, Ivor.TT | | freeze | Ivor.TT | | fun | Ivor.ViewTerm, Ivor.TT | | generalise | Ivor.TT | | GenRec | Ivor.TT | | getAllDefs | Ivor.TT | | getAllInductives | Ivor.TT | | getAllPatternDefs | Ivor.TT | | getAllTypes | Ivor.TT | | getApp | Ivor.ViewTerm, Ivor.TT | | getArgTypes | Ivor.ViewTerm, Ivor.TT | | getConstructorArity | Ivor.TT | | getConstructors | Ivor.TT | | getConstructorTag | Ivor.TT | | getContext | Ivor.Shell | | getDef | Ivor.TT | | getElimRule | Ivor.TT | | getError | Ivor.TT | | getFnArgs | Ivor.ViewTerm, Ivor.TT | | getGoal | Ivor.TT | | getGoals | Ivor.TT | | getInductive | Ivor.TT | | getPatternDef | Ivor.TT | | getReturnType | Ivor.ViewTerm, Ivor.TT | | getType | Ivor.TT | | Goal | Ivor.TT | | goal | Ivor.TT | | GoalData | Ivor.TT | | goalData | Ivor.TT | | goalName | Ivor.TT | | goalType | Ivor.TT | | hide | Ivor.TT | | Holey | Ivor.TT | | 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 | | IsData | Ivor.TT | | isItJust | Ivor.Construction | | IsTerm | Ivor.TT | | keepSolving | Ivor.TT | | Label | Ivor.ViewTerm, Ivor.TT | | labeltype | Ivor.ViewTerm, Ivor.TT | | Lambda | Ivor.ViewTerm, Ivor.TT | | left | Ivor.Construction | | Let | Ivor.ViewTerm, Ivor.TT | | load | Ivor.Plugin | | Message | Ivor.TT | | Metavar | Ivor.ViewTerm, Ivor.TT | | mkVar | Ivor.ViewTerm, Ivor.TT | | Name | | 1 (Type/Class) | Ivor.ViewTerm, Ivor.TT | | 2 (Data Constructor) | Ivor.ViewTerm, Ivor.TT | | name | Ivor.ViewTerm, Ivor.TT | | namesIn | Ivor.ViewTerm, Ivor.TT | | NameType | Ivor.ViewTerm, Ivor.TT | | nameType | Ivor.TT | | nametype | Ivor.ViewTerm, Ivor.TT | | newShell | Ivor.Shell | | NoSuchVar | Ivor.TT | | NotConvertible | Ivor.TT | | numUnsolved | Ivor.TT | | occursIn | Ivor.ViewTerm, Ivor.TT | | parameters | Ivor.ViewTerm, Ivor.TT | | parseDataString | Ivor.TermParser | | parsePrimitives | Ivor.Primitives | | parsePrimTerm | Ivor.Primitives | | parseTermString | Ivor.TermParser | | Partial | Ivor.TT | | Patterns | | 1 (Type/Class) | Ivor.TT | | 2 (Data Constructor) | Ivor.TT | | patterns | Ivor.TT | | PattOpt | Ivor.TT | | PClause | | 1 (Type/Class) | Ivor.TT | | 2 (Data Constructor) | Ivor.TT | | pInductive | Ivor.TermParser | | Placeholder | Ivor.ViewTerm, Ivor.TT | | pNoApp | Ivor.TermParser | | prefix | Ivor.Shell | | proofterm | Ivor.TT | | proving | Ivor.TT | | pTerm | Ivor.TermParser | | PWithClause | Ivor.TT | | qed | Ivor.TT | | Quote | Ivor.ViewTerm, Ivor.TT | | quotedterm | Ivor.ViewTerm, Ivor.TT | | quoteVal | Ivor.TT | | refine | Ivor.TT | | refineWith | Ivor.TT | | rename | Ivor.TT | | replace | Ivor.TT | | response | Ivor.Shell | | restore | Ivor.TT | | resume | Ivor.TT | | Return | Ivor.ViewTerm, Ivor.TT | | returnComputation | Ivor.TT | | returnterm | Ivor.ViewTerm, Ivor.TT | | returnval | Ivor.TT | | right | Ivor.Construction | | Rule | Ivor.TT | | runShell | Ivor.Shell | | save | Ivor.TT | | scope | Ivor.ViewTerm, Ivor.TT | | scrutinee | Ivor.TT | | sendCommand | Ivor.Shell | | sendCommandIO | Ivor.Shell | | shellParseTerm | Ivor.Shell | | ShellState | Ivor.Shell | | showProofState | Ivor.Shell | | solve | Ivor.TT | | split | Ivor.Construction | | Star | Ivor.ViewTerm, Ivor.TT | | subGoals | Ivor.TT | | subst | Ivor.ViewTerm, Ivor.TT | | suspend | Ivor.TT | | 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 | | 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 | | Unbound | Ivor.TT | | unfold | Ivor.TT | | uniqueName | Ivor.TT | | Unknown | Ivor.ViewTerm, Ivor.TT | | updateShell | Ivor.Shell | | useCon | Ivor.Construction | | var | Ivor.ViewTerm, Ivor.TT | | vartype | Ivor.ViewTerm, Ivor.TT | | varval | Ivor.ViewTerm, Ivor.TT | | view | Ivor.ViewTerm, Ivor.TT | | ViewConst | Ivor.ViewTerm, Ivor.TT | | ViewTerm | Ivor.ViewTerm, Ivor.TT | | viewType | Ivor.ViewTerm, Ivor.TT | | whnf | Ivor.TT |
|
