Index - I
| I | Idris.Core.TT |
| IBC | Idris.Imports |
| IBCAccess | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCAutoHint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCCG | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCCGFlag | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCCoercion | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCConstraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCData | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDeprecate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDyLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCErrRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCExtern | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFlags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFnInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFormat | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFragile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFunctionErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCHeader | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImportDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCInjective | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCKeyword | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCLineApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCMetaInformation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCModDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCNameHint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCObj | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCParsedRegion | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ibcPathNoFallback | Idris.Imports |
| IBCPhase | Idris.IBC |
| IBCPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCRecord | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCStatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCSubDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTotCheckErr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTrans | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCUsage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCWrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBC_Building | Idris.IBC |
| IBC_REPL | Idris.IBC |
| ibc_write | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ICodeGen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ICoverage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdeMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Idemode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdeModeCommand | Idris.IdeMode |
| ideModeEpoch | Idris.IdeMode |
| idemodePutSExp | Idris.Output |
| ideModeReturnAnnotated | Idris.Output |
| ideModeReturnWithStatus | Idris.Output |
| IdemodeSocket | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| identifier | Idris.Parser.Helpers, Idris.Parser |
| iderr | Idris.Elab.Utils |
| idiom | Idris.Parser.Expr, Idris.Parser |
| IDR | Idris.Imports |
| Idris | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris | Idris.REPL |
| idrisCatch | Idris.Error |
| IdrisColour | |
| 1 (Type/Class) | Idris.Colours |
| 2 (Data Constructor) | Idris.Colours |
| idrisInit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdrisInnerParser | |
| 1 (Type/Class) | Idris.Parser.Helpers, Idris.Parser |
| 2 (Data Constructor) | Idris.Parser.Helpers, Idris.Parser |
| idrisMain | Idris.REPL |
| IdrisParser | Idris.Parser.Helpers, Idris.Parser |
| idrisStyle | Idris.Parser.Helpers, Idris.Parser |
| idris_autohints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_callgraph | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_callswho | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_cgflags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_classes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_coercions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_colourRepl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_colourTheme | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_consolewidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_constraints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_datatypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_defertotcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_deprecated | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_docstrings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_dsls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_dynamic_libs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_erasureUsed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_errRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_exports | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_externs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_fixities | Idris.ASTUtils |
| idris_flags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_fninfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_fragile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_function_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_hdrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_highlightedRegions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_implicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_infixes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_inmodule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_language_extensions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_libs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_lineapps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_main | Idris.Package.Common |
| idris_metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_moduledocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_namehints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_nameIdx | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_objs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_openimpls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_optimisation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_options | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_opts | Idris.Package.Common |
| idris_outputmode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_parsedSpan | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_parserHighlights | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_patdefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_postulates | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_records | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_repl_defs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_scprims | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_statics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_symbols | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_tests | Idris.Package.Common |
| idris_totcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_totcheckfail | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_transforms | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_ttstats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_tyinfodata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_whocalls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IElab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IErasure | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ierror | Idris.Error |
| ifail | Idris.Error |
| IFileType | Idris.Imports |
| if_ | Idris.Parser.Expr, Idris.Parser |
| IIBC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Image | Idris.Docstrings |
| Imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| impIn | Idris.AbsSyntax |
| Impl | Idris.Core.TT |
| impl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Implicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| implicit | Idris.AbsSyntax |
| implicit' | Idris.AbsSyntax |
| implicitable | Idris.Core.TT |
| implicitAllowed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| implicitArg | Idris.Parser.Expr, Idris.Parser |
| ImplicitColour | Idris.Colours |
| implicitColour | Idris.Colours |
| ImplicitD | Idris.PartialEval |
| ImplicitInfo | Idris.Core.TT |
| implicitise | Idris.AbsSyntax |
| implicitNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| implicitPi | Idris.Parser.Expr, Idris.Parser |
| ImplicitS | Idris.PartialEval |
| implicit_warnings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| impl_gen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ImportDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| importDirs | IRTS.CodegenCommon |
| imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ImportInfo | |
| 1 (Type/Class) | Idris.Parser |
| 2 (Data Constructor) | Idris.Parser |
| import_ | Idris.Parser |
| import_location | Idris.Parser |
| import_modname_location | Idris.Parser |
| import_namespace | Idris.Parser |
| import_path | Idris.Parser |
| import_reexport | Idris.Parser |
| import_rename | Idris.Parser |
| Impossible | Idris.Core.TT |
| impossible | Idris.Parser.Expr, Idris.Parser |
| ImpossibleCase | Idris.Core.CaseTree |
| impShow | Idris.AbsSyntax |
| imp_methods | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Inaccessible | Idris.Core.TT |
| inaccessible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InaccessibleArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inaccessibleArgs | Idris.Elab.Utils |
| inaccessibleImps | Idris.Elab.Utils |
| iName | Idris.Parser.Helpers, Idris.Parser |
| inblock | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| includes | IRTS.CodegenCommon |
| IncompleteTerm | Idris.Core.TT |
| indent | |
| 1 (Function) | IRTS.DumpBC |
| 2 (Function) | Idris.Parser.Helpers, Idris.Parser |
| indented | Idris.Parser.Helpers, Idris.Parser |
| indentedBlock | Idris.Parser.Helpers, Idris.Parser |
| indentedBlock1 | Idris.Parser.Helpers, Idris.Parser |
| indentedBlockS | Idris.Parser.Helpers, Idris.Parser |
| IndentProperty | |
| 1 (Type/Class) | Idris.Parser.Helpers, Idris.Parser |
| 2 (Data Constructor) | Idris.Parser.Helpers, Idris.Parser |
| indentPropHolds | Idris.Parser.Helpers, Idris.Parser |
| indent_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| index_first | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| index_next | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Induction | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| induction | Idris.Core.Elaborate |
| inferCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferredDiff | Idris.Elab.Utils |
| InferredVal | Idris.Core.TT |
| inferTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infer_app | Idris.Core.Elaborate |
| InfinitelyWide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InfiniteUnify | Idris.Core.TT |
| Infixl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InfixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Infixr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initContext | Idris.Core.Evaluate |
| initDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initElabCtxt | Idris.Elab.Term |
| initElaborator | Idris.Core.Elaborate |
| initEState | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initEval | Idris.Core.Evaluate |
| initNextNameFrom | Idris.Core.Elaborate |
| initsEndAt | Idris.Parser.Helpers, Idris.Parser |
| injective | Idris.Core.ProofState, Idris.Core.Elaborate |
| Injectivity | Idris.Core.Evaluate |
| inl | IRTS.Inliner |
| Inlinable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inlinable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Inline | |
| 1 (Data Constructor) | IRTS.Lang, IRTS.Defunctionalise |
| 2 (Type/Class) | Idris.Docstrings |
| inline | IRTS.Inliner |
| inlineAll | IRTS.LangOpts |
| inlineDef | Idris.Inliner |
| inlineTerm | Idris.Inliner |
| inPattern | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inPkgDir | Idris.Package |
| installedPackages | Idris.Imports |
| installIBC | Idris.Package |
| installIdx | Idris.Package |
| installObj | Idris.Package |
| installPkg | Idris.Package |
| Instance | Idris.Core.ProofState, Idris.Core.Elaborate |
| instanceArg | Idris.Core.Elaborate |
| instanceBlock | Idris.Parser |
| InstanceCtorN | Idris.Core.TT |
| instanceCtorName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InstanceN | Idris.Core.TT |
| instances | Idris.Core.ProofState, Idris.Core.Elaborate |
| instance_ | Idris.Parser |
| instantiate | Idris.Core.TT |
| integer | Idris.Parser.Helpers, Idris.Parser |
| IntegerAtom | Idris.IdeMode |
| integerReader | Idris.CmdOptions |
| Interface | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| interfaces | IRTS.CodegenCommon |
| interMap | IRTS.DumpBC |
| internalDecl | Idris.Parser |
| internalExpr | Idris.Parser.Expr, Idris.Parser |
| InternalMsg | Idris.Core.TT |
| internalNS | Idris.Core.TT |
| Interpret | Idris.IdeMode |
| InterpretScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Intro | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| intro | Idris.Core.Elaborate |
| Intros | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IntroTy | Idris.Core.ProofState, Idris.Core.Elaborate |
| introTy | Idris.Core.Elaborate |
| intToReflectedNat | Idris.Reflection |
| IntTy | Idris.Core.TT |
| intTyName | Idris.Core.TT |
| invalidOperators | Idris.Parser.Helpers, Idris.Parser |
| InvalidTCArg | Idris.Core.TT |
| IOption | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IParse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| iPrintError | Idris.Output |
| iPrintFunTypes | Idris.Output |
| iPrintResult | Idris.Output |
| iPrintTermWithType | Idris.Output |
| iPrintWithStatus | Idris.Output |
| iputGoal | Idris.Output |
| iputStrLn | Idris.Output |
| iRender | Idris.Output |
| iRenderError | Idris.Output |
| iRenderOutput | Idris.Output |
| iRenderResult | Idris.Output |
| IRFormat | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isATTY | Util.System |
| isCanonical | Idris.Core.Evaluate |
| isConName | Idris.Core.Evaluate |
| isConst | IRTS.Bytecode |
| isDConName | Idris.Core.Evaluate |
| isEol | Idris.Parser.Helpers, Idris.Parser |
| isetLoadedRegion | Idris.AbsSyntax |
| isetPrompt | Idris.AbsSyntax |
| isFnName | Idris.Core.Evaluate |
| isHole | Idris.Core.Typecheck |
| isHoleName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isInjective | Idris.Core.TT |
| isMetavarName | Idris.AbsSyntax |
| isPlausible | Idris.Elab.Term |
| isPostulateName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IState | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isTCDict | Idris.Core.Evaluate |
| isTConName | Idris.Core.Evaluate |
| IsTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isTyInferred | Idris.AbsSyntax |
| IsType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isType | Idris.Core.Typecheck |
| isTypeConst | Idris.Core.TT |
| ist_callgraph | Idris.ASTUtils |
| ist_optimisation | Idris.ASTUtils |
| isUndefined | Idris.AbsSyntax |
| isUniverse | Idris.Core.Evaluate |
| isWindows | Util.System |
| is_guess | Idris.Core.Elaborate |
| is_scoped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IT16 | Idris.Core.TT |
| IT32 | Idris.Core.TT |
| IT64 | Idris.Core.TT |
| IT8 | Idris.Core.TT |
| italic | Idris.Colours |
| ItalicText | Idris.Core.TT |
| ITBig | Idris.Core.TT |
| ITChar | Idris.Core.TT |
| ITFixed | Idris.Core.TT |
| ITNative | Idris.Core.TT |
| Itself | Idris.Core.Evaluate |
| iucheck | Idris.Error |
| iWarn | Idris.Output |