| 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 |
| addBinder | Idris.Core.TT |
| addCasedef | Idris.Core.Evaluate |
| addClass | Idris.AbsSyntax |
| AddClause | Idris.IdeSlave |
| AddClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| addErrRev | 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.IdeSlave |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addNameHint | Idris.AbsSyntax |
| addNameIdx | Idris.AbsSyntax |
| addNameIdx' | Idris.AbsSyntax |
| addObjectFile | Idris.AbsSyntax |
| addOperator | Idris.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 | Idris.Core.Evaluate |
| ADDTOP | IRTS.Bytecode |
| addTrans | Idris.AbsSyntax |
| addTyDecl | Idris.Core.Evaluate |
| addTyInfConstraints | Idris.AbsSyntax |
| addTyInferred | Idris.AbsSyntax |
| 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 | Idris.Core.TT |
| alt | Idris.ParseExpr, Idris.Parser |
| AnnBoundName | Idris.Core.TT |
| AnnConstData | Idris.Core.TT |
| AnnConstType | Idris.Core.TT |
| AnnFC | Idris.Core.TT |
| AnnKeyword | Idris.Core.TT |
| AnnName | Idris.Core.TT |
| AnnTextFmt | 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 |
| applyDataOpt | Idris.DataOpts |
| applyDataOptRT | Idris.DataOpts |
| applyOpts | Idris.DataOpts |
| ApplyTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| apply_elab | Idris.Core.Elaborate |
| Apropos | |
| 1 (Data Constructor) | Idris.IdeSlave |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 3 (Type/Class) | Idris.Apropos |
| apropos | Idris.Apropos |
| arg | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| argExpr | Idris.Parser |
| ArgOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsdef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsused | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ArithTy | Idris.Core.TT |
| arithTyToJType | IRTS.Java.JTypes |
| arity | Idris.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 | Idris.Core.TT |
| ATFloat | Idris.Core.TT |
| 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 |
| AutomaticWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AutoSolve | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AutoWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |