| Abandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| accData | Idris.ParseHelpers, Idris.Parser |
| Accessibility | Core.Evaluate |
| accessibility | Idris.ParseHelpers, Idris.Parser |
| addAcc | Idris.ParseHelpers, Idris.Parser |
| addAlist | Core.TT |
| addApps | IRTS.Defunctionalise |
| addBinder | Core.TT |
| addCasedef | Core.Evaluate |
| addClass | Idris.AbsSyntax |
| AddClause | Idris.IdeSlave |
| AddClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addCoercion | Idris.AbsSyntax |
| addConstraints | Idris.AbsSyntax |
| addCtxtDef | Core.Evaluate |
| addDatatype | Core.Evaluate |
| addDef | Core.TT |
| addDeferred | Idris.AbsSyntax |
| addDeferred' | Idris.AbsSyntax |
| addDeferredTyCon | Idris.AbsSyntax |
| addDocStr | Idris.AbsSyntax |
| addDyLib | Idris.AbsSyntax |
| addFlag | Idris.AbsSyntax |
| addFn | IRTS.Lang, IRTS.Defunctionalise |
| 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 |
| addInstance | Idris.AbsSyntax |
| addInternalApp | Idris.AbsSyntax |
| addLangExt | Idris.AbsSyntax |
| addLib | Idris.AbsSyntax |
| AddMissing | |
| 1 (Data Constructor) | Idris.IdeSlave |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addObjectFile | Idris.AbsSyntax |
| addOperator | Core.Evaluate |
| AddProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AddProofClause | Idris.IdeSlave |
| AddProofClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addStatics | Idris.AbsSyntax |
| addTags | IRTS.Lang, IRTS.Defunctionalise |
| addToBlock | IRTS.Java.ASTBuilding |
| addToCalledG | Idris.AbsSyntax |
| addToCG | Idris.AbsSyntax |
| addToCtxt | Core.Evaluate |
| ADDTOP | IRTS.Bytecode |
| addTrans | Idris.AbsSyntax |
| addTyDecl | Core.Evaluate |
| addUsingConstraints | Idris.AbsSyntax |
| aiFn | Idris.AbsSyntax |
| allImportDirs | Idris.AbsSyntax |
| allNames | Idris.AbsSyntax |
| allNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| allNothing | Idris.Coverage |
| allowImp | Idris.ParseExpr, Idris.Parser |
| AlreadyDefined | Core.TT |
| alt | Idris.ParseExpr, Idris.Parser |
| AnySyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| App | Core.TT |
| app | Idris.ParseExpr, Idris.Parser |
| apply | Core.Elaborate |
| apply' | Core.Elaborate |
| apply2 | Core.Elaborate |
| ApplyCase | IRTS.Defunctionalise |
| applyDataOpt | Idris.DataOpts |
| applyDataOptRT | Idris.DataOpts |
| applyOpts | Idris.DataOpts |
| ApplyTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| apply_elab | Core.Elaborate |
| arg | |
| 1 (Function) | Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| argExpr | Idris.Parser |
| argsdef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsused | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ArithTy | Core.TT |
| arithTyToJType | IRTS.Java.JTypes |
| arity | Core.TT |
| array | IRTS.Java.JTypes |
| arrayInitExps | IRTS.Java.ASTBuilding |
| arraysType | IRTS.Java.JTypes |
| AssertTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ASSIGN | IRTS.Bytecode |
| assign | IRTS.Bytecode |
| ASSIGNCONST | IRTS.Bytecode |
| assumptionNames | Idris.Prover |
| At | Core.TT |
| ATFloat | Core.TT |
| ATInt | Core.TT |
| Attack | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| attack | Core.Elaborate |
| AType | Core.TT |