| Abandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| accData | Idris.ParseHelpers, Idris.Parser |
| Accessibility | Idris.Core.Evaluate |
| accessibility | Idris.ParseHelpers, Idris.Parser |
| addAcc | Idris.ParseHelpers, Idris.Parser |
| addAlist | Idris.Core.TT |
| addApps | IRTS.Defunctionalise |
| addAutoImport | Idris.AbsSyntax |
| addBinder | Idris.Core.TT |
| addCasedef | Idris.Core.Evaluate |
| addClass | Idris.AbsSyntax |
| AddClause | Idris.IdeMode |
| AddClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addClauseFrom | Idris.Interactive |
| addCoercion | Idris.AbsSyntax |
| addConstraints | Idris.AbsSyntax |
| addCtxtDef | Idris.Core.Evaluate |
| addDatatype | Idris.Core.Evaluate |
| addDef | Idris.Core.TT |
| addDeferred | Idris.AbsSyntax |
| addDeferred' | Idris.AbsSyntax |
| addDeferredTyCon | Idris.AbsSyntax |
| addDocStr | Idris.AbsSyntax |
| addDyLib | Idris.AbsSyntax |
| addErasureUsage | Idris.AbsSyntax |
| addErrRev | Idris.AbsSyntax |
| addExport | Idris.AbsSyntax |
| addFlag | Idris.AbsSyntax |
| addFn | IRTS.Lang, IRTS.Defunctionalise |
| addFunctionErrorHandlers | Idris.AbsSyntax |
| addHdr | Idris.AbsSyntax |
| addHides | Idris.Parser |
| addIBC | Idris.AbsSyntax |
| addImpl | Idris.AbsSyntax |
| addImpl' | Idris.AbsSyntax |
| addImplBound | Idris.AbsSyntax |
| addImplBoundInf | Idris.AbsSyntax |
| addImplPat | Idris.AbsSyntax |
| addImportDir | Idris.AbsSyntax |
| addImported | Idris.AbsSyntax |
| addInstance | Idris.AbsSyntax |
| addInternalApp | Idris.AbsSyntax |
| addLangExt | Idris.AbsSyntax |
| addLib | Idris.AbsSyntax |
| AddMissing | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| addMissing | Idris.Interactive |
| addNameHint | Idris.AbsSyntax |
| addNameIdx | Idris.AbsSyntax |
| addNameIdx' | Idris.AbsSyntax |
| addObjectFile | Idris.AbsSyntax |
| addOperator | Idris.Core.Evaluate |
| AddOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addOptimise | Idris.AbsSyntax |
| AddProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AddProofClause | Idris.IdeMode |
| AddProofClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addProofClauseFrom | Idris.Interactive |
| addReplSyntax | Idris.Parser |
| addStatics | Idris.AbsSyntax |
| addSyntax | Idris.Parser |
| addTags | IRTS.Lang, IRTS.Defunctionalise |
| addToCalledG | Idris.AbsSyntax |
| addToCG | Idris.AbsSyntax |
| addToCtxt | Idris.Core.Evaluate |
| ADDTOP | IRTS.Bytecode |
| addToUsing | Idris.AbsSyntax |
| addTrans | Idris.AbsSyntax |
| addTyDecl | Idris.Core.Evaluate |
| addTyInfConstraints | Idris.AbsSyntax |
| addTyInferred | Idris.AbsSyntax |
| addUsedName | Idris.AbsSyntax |
| addUsingConstraints | Idris.AbsSyntax |
| addUsingImpls | Idris.AbsSyntax |
| aiFn | Idris.AbsSyntax |
| allHelp | Idris.REPLParser |
| allImportDirs | Idris.AbsSyntax |
| allNames | Idris.AbsSyntax |
| allNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| allNothing | Idris.Coverage |
| allocUnique | IRTS.Lang, IRTS.Defunctionalise |
| allowImp | Idris.ParseExpr, Idris.Parser |
| allTTNames | Idris.Core.TT |
| AllTypes | Idris.Core.TT |
| AlreadyDefined | Idris.Core.TT |
| alt | Idris.ParseExpr, Idris.Parser |
| AltsTArg | Idris.ParseExpr, Idris.Parser |
| AlwaysShow | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AnnBoundName | Idris.Core.TT |
| AnnConst | Idris.Core.TT |
| AnnData | Idris.Core.TT |
| AnnErr | Idris.Core.TT |
| AnnFC | Idris.Core.TT |
| AnnKeyword | Idris.Core.TT |
| AnnName | Idris.Core.TT |
| annName | Idris.Delaborate |
| annotCode | Idris.Docstrings |
| AnnSearchResult | Idris.Core.TT |
| AnnTerm | Idris.Core.TT |
| AnnTextFmt | Idris.Core.TT |
| AnnType | Idris.Core.TT |
| AnySyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| App | Idris.Core.TT |
| app | Idris.ParseExpr, Idris.Parser |
| apply | Idris.Core.Elaborate |
| apply' | Idris.Core.Elaborate |
| apply2 | Idris.Core.Elaborate |
| ApplyCase | IRTS.Defunctionalise |
| applyDataOptRT | Idris.DataOpts |
| applyOpts | Idris.DataOpts |
| ApplyTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| applyTransRules | Idris.Transforms |
| applyTransRulesWith | Idris.Transforms |
| apply_elab | Idris.Core.Elaborate |
| Apropos | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| apropos | Idris.Apropos |
| aproposModules | Idris.Apropos |
| arg | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| argExpr | Idris.Parser |
| argName | Idris.Reflection |
| ArgOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsdef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsused | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argTy | Idris.Reflection |
| ArithTy | Idris.Core.TT |
| arity | Idris.Core.TT |
| AssertTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ASSIGN | IRTS.Bytecode |
| assign | IRTS.Bytecode |
| ASSIGNCONST | IRTS.Bytecode |
| assumptionNames | Idris.Prover |
| At | Idris.Core.TT |
| ATFloat | Idris.Core.TT |
| atHole | Idris.Core.ProofTerm |
| ATInt | Idris.Core.TT |
| Attack | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| attack | Idris.Core.Elaborate |
| AType | Idris.Core.TT |
| AutoArg | Idris.Core.ProofState, Idris.Core.Elaborate |
| autoArg | Idris.Core.Elaborate |
| AutomaticWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| autos | Idris.Core.ProofState, Idris.Core.Elaborate |
| AutoSolve | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AutoWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |