idris-1.0: Functional Programming Language with Dependent Types

Index - I

IIdris.Core.TT
IBCIdris.Imports
IBCAccessIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCAutoHintIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCCGIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCCGFlagIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCCoercionIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCConstraintIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCDataIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCDefIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCDeprecateIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCDocIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCDSLIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCDyLibIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCErrorHandlerIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCErrReduceIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCErrRevIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCExportIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCExternIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCFixIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCFlagsIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCFnInfoIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCFormatIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCFragileIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCFunctionErrorHandlerIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCHeaderIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCImpIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCImplementationIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCImportIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCImportDirIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCInjectiveIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCInterfaceIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCKeywordIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCLibIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCLineAppIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCMetaInformationIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCMetavarIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCModDocsIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCNameHintIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCObjIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCOptIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCParsedRegionIdris.AbsSyntaxTree, Idris.AbsSyntax
ibcPathNoFallbackIdris.Imports
IBCPhaseIdris.IBC
IBCPostulateIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCRecordIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCSourceDirIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCStaticIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCSubDirIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCSyntaxIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCTotalIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCTotCheckErrIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCTransIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCUsageIdris.AbsSyntaxTree, Idris.AbsSyntax
IBCWriteIdris.AbsSyntaxTree, Idris.AbsSyntax
IBC_BuildingIdris.IBC
IBC_REPLIdris.IBC
ibc_writeIdris.AbsSyntaxTree, Idris.AbsSyntax
ICodeGenIdris.AbsSyntaxTree, Idris.AbsSyntax
ICoverageIdris.AbsSyntaxTree, Idris.AbsSyntax
IdeModeIdris.AbsSyntaxTree, Idris.AbsSyntax
IdemodeIdris.AbsSyntaxTree, Idris.AbsSyntax
IdeModeCommandIdris.IdeMode
ideModeEpochIdris.IdeMode
idemodePutSExpIdris.Output
ideModeReturnAnnotatedIdris.Output
ideModeReturnWithStatusIdris.Output
IdemodeSocketIdris.AbsSyntaxTree, Idris.AbsSyntax
idemodeStartIdris.REPL
identifierIdris.Parser.Helpers, Idris.Parser
iderrIdris.Elab.Utils
idiomIdris.Parser.Expr, Idris.Parser
IDRIdris.Imports
IdrisIdris.AbsSyntaxTree, Idris.AbsSyntax
idrisIdris.Main
idrisCatchIdris.Error
IdrisColour 
1 (Type/Class)Idris.Colours
2 (Data Constructor)Idris.Colours
idrisInitIdris.AbsSyntaxTree, Idris.AbsSyntax
IdrisInnerParser 
1 (Type/Class)Idris.Parser.Helpers, Idris.Parser
2 (Data Constructor)Idris.Parser.Helpers, Idris.Parser
idrisMainIdris.Main
IdrisParserIdris.Parser.Helpers, Idris.Parser
idrisStyleIdris.Parser.Helpers, Idris.Parser
idris_autohintsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_callgraphIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_cgflagsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_coercionsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_colourReplIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_colourThemeIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_consolewidthIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_constraintsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_datatypesIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_defertotcheckIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_deprecatedIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_docstringsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_dslsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_dynamic_libsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_erasureUsedIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_errorhandlersIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_errReduceIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_errRevIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_exportsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_externsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_fixitiesIdris.ASTUtils
idris_flagsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_fninfoIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_fragileIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_function_errorhandlersIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_hdrsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_highlightedRegionsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_implicitsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_importedIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_infixesIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_inmoduleIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_interactiveOptsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_interfacesIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_language_extensionsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_libsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_lineappsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_mainIdris.Package.Common
idris_metavarsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_moduledocsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_nameIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_namehintsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_nameIdxIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_objsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_openimplsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_optimisationIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_optionsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_optsIdris.Package.Common
idris_outputmodeIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_parsedSpanIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_parserHighlightsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_patdefsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_postulatesIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_recordsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_repl_defsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_scprimsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_staticsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_symbolsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_testsIdris.Package.Common
idris_totcheckIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_totcheckfailIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_transformsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_ttstatsIdris.AbsSyntaxTree, Idris.AbsSyntax
idris_tyinfodataIdris.AbsSyntaxTree, Idris.AbsSyntax
IElabIdris.AbsSyntaxTree, Idris.AbsSyntax
IErasureIdris.AbsSyntaxTree, Idris.AbsSyntax
ierrorIdris.Error
ifailIdris.Error
IFileTypeIdris.Imports
if_Idris.Parser.Expr, Idris.Parser
IIBCIdris.AbsSyntaxTree, Idris.AbsSyntax
ImageIdris.Docstrings
ImpIdris.AbsSyntaxTree, Idris.AbsSyntax
impInIdris.AbsSyntax
ImplIdris.Core.TT
implIdris.AbsSyntaxTree, Idris.AbsSyntax
ImplementationIdris.Core.ProofState, Idris.Core.Elaborate
implementationIdris.Parser
implementationArgIdris.Core.Elaborate
implementationBlockIdris.Parser
ImplementationCtorNIdris.Core.TT
implementationCtorNameIdris.AbsSyntaxTree, Idris.AbsSyntax
ImplementationNIdris.Core.TT
implementationsIdris.Core.ProofState, Idris.Core.Elaborate
ImplicitIdris.AbsSyntaxTree, Idris.AbsSyntax
implicitIdris.AbsSyntax
implicit'Idris.AbsSyntax
implicitableIdris.Core.TT
implicitAllowedIdris.AbsSyntaxTree, Idris.AbsSyntax
implicitArgIdris.Parser.Expr, Idris.Parser
ImplicitColourIdris.Colours
implicitColourIdris.Colours
ImplicitDIdris.PartialEval
ImplicitInfoIdris.Core.TT
implicitiseIdris.AbsSyntax
implicitNamesInIdris.AbsSyntaxTree, Idris.AbsSyntax
implicitPiIdris.Parser.Expr, Idris.Parser
ImplicitSIdris.PartialEval
implicit_warningsIdris.AbsSyntaxTree, Idris.AbsSyntax
impl_genIdris.AbsSyntaxTree, Idris.AbsSyntax
ImportDirIdris.AbsSyntaxTree, Idris.AbsSyntax
importDirsIRTS.CodegenCommon
importedIdris.AbsSyntaxTree, Idris.AbsSyntax
ImportInfo 
1 (Type/Class)Idris.Parser
2 (Data Constructor)Idris.Parser
import_Idris.Parser
import_locationIdris.Parser
import_modname_locationIdris.Parser
import_namespaceIdris.Parser
import_pathIdris.Parser
import_reexportIdris.Parser
import_renameIdris.Parser
ImpossibleIdris.Core.TT
impossibleIdris.Parser.Expr, Idris.Parser
ImpossibleCaseIdris.Core.CaseTree
impShowIdris.AbsSyntax
imp_methodsIdris.AbsSyntaxTree, Idris.AbsSyntax
InaccessibleIdris.Core.TT
inaccessibleIdris.AbsSyntaxTree, Idris.AbsSyntax
InaccessibleArgIdris.AbsSyntaxTree, Idris.AbsSyntax
inaccessibleArgsIdris.Elab.Utils
inaccessibleImpsIdris.Elab.Utils
iNameIdris.Parser.Helpers, Idris.Parser
inblockIdris.AbsSyntaxTree, Idris.AbsSyntax
includesIRTS.CodegenCommon
IncompleteTermIdris.Core.TT
indent 
1 (Function)Idris.Parser.Helpers, Idris.Parser
2 (Function)IRTS.DumpBC
IndentClauseIdris.AbsSyntaxTree, Idris.AbsSyntax
indentedIdris.Parser.Helpers, Idris.Parser
indentedBlockIdris.Parser.Helpers, Idris.Parser
indentedBlock1Idris.Parser.Helpers, Idris.Parser
indentedBlockSIdris.Parser.Helpers, Idris.Parser
IndentProperty 
1 (Type/Class)Idris.Parser.Helpers, Idris.Parser
2 (Data Constructor)Idris.Parser.Helpers, Idris.Parser
indentPropHoldsIdris.Parser.Helpers, Idris.Parser
IndentWithIdris.AbsSyntaxTree, Idris.AbsSyntax
indent_stackIdris.AbsSyntaxTree, Idris.AbsSyntax
index_firstIdris.AbsSyntaxTree, Idris.AbsSyntax
index_nextIdris.AbsSyntaxTree, Idris.AbsSyntax
Induction 
1 (Data Constructor)Idris.Core.ProofState, Idris.Core.Elaborate
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
inductionIdris.Core.Elaborate
inferConIdris.AbsSyntaxTree, Idris.AbsSyntax
inferDeclIdris.AbsSyntaxTree, Idris.AbsSyntax
inferOptsIdris.AbsSyntaxTree, Idris.AbsSyntax
InferredIdris.Core.TT
inferredDiffIdris.Elab.Utils
InferredValIdris.Core.TT
inferTyIdris.AbsSyntaxTree, Idris.AbsSyntax
infer_appIdris.Core.Elaborate
InfinitelyWideIdris.AbsSyntaxTree, Idris.AbsSyntax
InfiniteUnifyIdris.Core.TT
InfixlIdris.AbsSyntaxTree, Idris.AbsSyntax
InfixNIdris.AbsSyntaxTree, Idris.AbsSyntax
InfixrIdris.AbsSyntaxTree, Idris.AbsSyntax
infPIdris.AbsSyntaxTree, Idris.AbsSyntax
infTermIdris.AbsSyntaxTree, Idris.AbsSyntax
initContextIdris.Core.Evaluate
initDSLIdris.AbsSyntaxTree, Idris.AbsSyntax
initElabCtxtIdris.Elab.Term
initElaboratorIdris.Core.Elaborate
initEStateIdris.AbsSyntaxTree, Idris.AbsSyntax
initEvalIdris.Core.Evaluate
initialInteractiveOptsIdris.AbsSyntaxTree, Idris.AbsSyntax
initNextNameFromIdris.Core.Elaborate
initsEndAtIdris.Parser.Helpers, Idris.Parser
injectiveIdris.Core.ProofState, Idris.Core.Elaborate
InjectivityIdris.Core.Evaluate
inlIRTS.Inliner
InlinableIdris.AbsSyntaxTree, Idris.AbsSyntax
inlinableIdris.AbsSyntaxTree, Idris.AbsSyntax
Inline 
1 (Type/Class)Idris.Docstrings
2 (Data Constructor)IRTS.Lang, IRTS.Defunctionalise
inlineIRTS.Inliner
inlineAllIRTS.LangOpts
inlineDefIdris.Inliner
inlineSmallIdris.Core.Evaluate
inlineTermIdris.Inliner
inPatternIdris.AbsSyntaxTree, Idris.AbsSyntax
inPkgDirIdris.Package
installedPackagesIdris.Imports
installIBCIdris.Package
installIdxIdris.Package
installObjIdris.Package
installPkgIdris.Package
instantiateIdris.Core.TT
integerIdris.Parser.Helpers, Idris.Parser
IntegerAtomIdris.IdeMode
integerReaderIdris.CmdOptions
InteractiveOpts 
1 (Type/Class)Idris.AbsSyntaxTree, Idris.AbsSyntax
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
interactiveOpts_indentClauseIdris.AbsSyntaxTree, Idris.AbsSyntax
interactiveOpts_indentWithIdris.AbsSyntaxTree, Idris.AbsSyntax
InterfaceIdris.AbsSyntaxTree, Idris.AbsSyntax
interfaceBlockIdris.Parser
InterfaceDocIdris.Docs
InterfaceInfoIdris.AbsSyntaxTree, Idris.AbsSyntax
interfacesIRTS.CodegenCommon
interface_Idris.Parser
interface_constraintsIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_defaultsIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_default_super_interfacesIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_determinersIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_implementationsIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_impparamsIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_methodsIdris.AbsSyntaxTree, Idris.AbsSyntax
interface_paramsIdris.AbsSyntaxTree, Idris.AbsSyntax
interMapIRTS.DumpBC
internalDeclIdris.Parser
internalExprIdris.Parser.Expr, Idris.Parser
InternalMsgIdris.Core.TT
internalNSIdris.Core.TT
InterpretIdris.IdeMode
InterpretScriptIdris.AbsSyntaxTree, Idris.AbsSyntax
Intro 
1 (Data Constructor)Idris.Core.ProofState, Idris.Core.Elaborate
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
introIdris.Core.Elaborate
IntrosIdris.AbsSyntaxTree, Idris.AbsSyntax
IntroTyIdris.Core.ProofState, Idris.Core.Elaborate
introTyIdris.Core.Elaborate
intToReflectedNatIdris.Reflection
IntTyIdris.Core.TT
intTyNameIdris.Core.TT
invalidOperatorsIdris.Parser.Helpers, Idris.Parser
InvalidTCArgIdris.Core.TT
IOption 
1 (Type/Class)Idris.AbsSyntaxTree, Idris.AbsSyntax
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
IParseIdris.AbsSyntaxTree, Idris.AbsSyntax
iPrintErrorIdris.Output
iPrintFunTypesIdris.Output
iPrintResultIdris.Output
iPrintTermWithTypeIdris.Output
iPrintWithStatusIdris.Output
iputGoalIdris.Output
iputStrIdris.Output
iputStrLnIdris.Output
iRenderIdris.Output
iRenderErrorIdris.Output
iRenderOutputIdris.Output
iRenderResultIdris.Output
iReportIdris.AbsSyntax
IRFormatIdris.AbsSyntaxTree, Idris.AbsSyntax
isATTYUtil.System
isCanonicalIdris.Core.Evaluate
isConNameIdris.Core.Evaluate
isConstIRTS.Bytecode
isDConNameIdris.Core.Evaluate
isEmptyIdris.Elab.Utils
isEolIdris.Parser.Helpers, Idris.Parser
isetLoadedRegionIdris.AbsSyntax
isetPromptIdris.AbsSyntax
isFnNameIdris.Core.Evaluate
isHoleIdris.Core.Typecheck
isHoleNameIdris.AbsSyntaxTree, Idris.AbsSyntax
isInjectiveIdris.Core.TT
isMetavarNameIdris.AbsSyntax
isPlausibleIdris.Elab.Utils
isPostulateNameIdris.AbsSyntaxTree, Idris.AbsSyntax
IState 
1 (Type/Class)Idris.AbsSyntaxTree, Idris.AbsSyntax
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
isTCDictIdris.Core.Evaluate
isTConNameIdris.Core.Evaluate
IsTermIdris.AbsSyntaxTree, Idris.AbsSyntax
isTyInferredIdris.AbsSyntax
IsTypeIdris.AbsSyntaxTree, Idris.AbsSyntax
isTypeIdris.Core.Typecheck
isTypeConstIdris.Core.TT
ist_callgraphIdris.ASTUtils
ist_optimisationIdris.ASTUtils
isUndefinedIdris.AbsSyntax
isUniverseIdris.Core.Evaluate
isWindowsUtil.System
is_guessIdris.Core.Elaborate
is_scopedIdris.AbsSyntaxTree, Idris.AbsSyntax
IT16Idris.Core.TT
IT32Idris.Core.TT
IT64Idris.Core.TT
IT8Idris.Core.TT
italicIdris.Colours
ItalicTextIdris.Core.TT
ITBigIdris.Core.TT
ITCharIdris.Core.TT
ITFixedIdris.Core.TT
ITNativeIdris.Core.TT
ItselfIdris.Core.Evaluate
iucheckIdris.Error
iWarnIdris.Output