Index
| $$ | Util.Pretty |
| $+$ | Util.Pretty |
| <+> | Util.Pretty |
| <> | |
| 1 (Function) | Util.Pretty |
| 2 (Function) | IRTS.Java.ASTBuilding |
| @! | IRTS.Java.ASTBuilding |
| @:= | IRTS.Java.ASTBuilding |
| 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 |
| B16 | Core.TT |
| B16V | Core.TT |
| B32 | Core.TT |
| B32V | Core.TT |
| B64 | Core.TT |
| B64V | Core.TT |
| B8 | Core.TT |
| B8V | Core.TT |
| backtick | Idris.ParseOps, Idris.Parser |
| banner | Idris.REPL |
| BASETOP | IRTS.Bytecode |
| BC | |
| 1 (Type/Class) | IRTS.BCImp |
| 2 (Type/Class) | IRTS.Bytecode |
| bc | |
| 1 (Function) | IRTS.BCImp |
| 2 (Function) | IRTS.Bytecode |
| BCAsm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| BelieveMe | Core.Evaluate |
| BI | Core.TT |
| bi | Idris.AbsSyntax |
| Bigger | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bigInteger | IRTS.Java.ASTBuilding |
| bigIntegerType | IRTS.Java.JTypes |
| binary | Idris.ParseOps, Idris.Parser |
| Bind | Core.TT |
| bindAll | Core.TT |
| Binder | Core.TT |
| binderTy | Core.TT |
| binderVal | Core.TT |
| Binding | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bindList | Idris.ParseHelpers, Idris.Parser |
| bindTyArgs | Core.TT |
| bold | Idris.Colours |
| BoolAtom | Idris.IdeSlave |
| Bound | Core.TT |
| BoundVarColour | Idris.Colours |
| boundVarColour | Idris.Colours |
| box | IRTS.Java.JTypes |
| braces | Util.Pretty |
| brace_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bracketed | Idris.ParseExpr, Idris.Parser |
| brackets | Util.Pretty |
| breakingSize | Util.Pretty |
| bugaddr | Idris.Delaborate |
| build | |
| 1 (Function) | Idris.ElabTerm |
| 2 (Function) | IRTS.Compiler |
| buildMods | Pkg.Package |
| buildPkg | Pkg.Package |
| buildSCG | Idris.Coverage |
| buildSCG' | Idris.Coverage |
| buildTC | Idris.ElabTerm |
| buildTree | Idris.Chaser |
| Bytecode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| byteType | IRTS.Java.JTypes |
| CA | Idris.ElabDecls |
| caf | Idris.Parser |
| calcProd | Idris.Coverage |
| calcTotality | Idris.Coverage |
| CALL | IRTS.Bytecode |
| call | IRTS.Java.ASTBuilding |
| Callable | IRTS.Java.ASTBuilding |
| callableType | IRTS.Java.JTypes |
| calls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CantConvert | Core.TT |
| CantInferType | Core.TT |
| CantIntroduce | Core.TT |
| CantResolve | Core.TT |
| CantResolveAlts | Core.TT |
| CantUnify | Core.TT |
| CASE | IRTS.Bytecode |
| Case | Core.CaseTree |
| CaseAlt | Core.CaseTree |
| caseAlt | IRTS.Bytecode |
| CaseAlt' | Core.CaseTree |
| CaseDef | |
| 1 (Type/Class) | Core.CaseTree |
| 2 (Data Constructor) | Core.CaseTree |
| CaseDefs | |
| 1 (Type/Class) | Core.Evaluate |
| 2 (Data Constructor) | Core.Evaluate |
| caseExpr | Idris.ParseExpr, Idris.Parser |
| CaseInfo | |
| 1 (Type/Class) | Core.Evaluate |
| 2 (Data Constructor) | Core.Evaluate |
| CaseN | Core.TT |
| CaseOp | Core.Evaluate |
| caseOption | Idris.ParseExpr, Idris.Parser |
| CaseSplit | Idris.IdeSlave |
| CaseSplitAt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| cases_compiletime | Core.Evaluate |
| cases_inlined | Core.Evaluate |
| cases_runtime | Core.Evaluate |
| cases_totcheck | Core.Evaluate |
| CaseTrans | Idris.Transforms |
| CaseTree | Core.CaseTree |
| case_inlinable | Core.Evaluate |
| cat | Util.Pretty |
| catchIO | Util.System |
| CExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CGInfo | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ch | Core.TT |
| ChangeDirectory | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| char | |
| 1 (Function) | Util.Pretty |
| 2 (Function) | Idris.ParseHelpers, Idris.Parser |
| charLiteral | Idris.ParseHelpers, Idris.Parser |
| charType | IRTS.Java.JTypes |
| Check | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| check | Core.Typecheck |
| check' | Core.Typecheck |
| CheckConv | Core.TT |
| checkDeclTotality | Idris.Coverage |
| checkDef | Idris.ElabDecls |
| checkDefs | IRTS.Simplified |
| checkDSL | Idris.ParseData, Idris.Parser |
| CheckIn | Core.ProofState, Core.Elaborate |
| checkInferred | Idris.ElabDecls |
| checkInjective | Core.Elaborate |
| checkMP | Idris.Coverage |
| checkPiGoal | Core.Elaborate |
| checkPositive | Idris.Coverage |
| checkPossible | Idris.ElabDecls |
| checkProgram | Core.Typecheck |
| checkSizeChange | Idris.Coverage |
| checkTotality | Idris.Coverage |
| checkUndefined | Idris.AbsSyntax |
| check_in | Core.Elaborate |
| Chr | Util.Pretty |
| CI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Claim | Core.ProofState, Core.Elaborate |
| claim | Core.Elaborate |
| ClassDoc | Idris.Docs |
| ClassInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| classInfo | Idris.REPL |
| class_ | Idris.Parser |
| class_defaults | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_instances | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_methods | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_params | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| clause | Idris.Parser |
| clean | |
| 1 (Function) | IRTS.Bytecode |
| 2 (Function) | Pkg.Package |
| cleanPkg | Pkg.Package |
| clearErr | Idris.AbsSyntax |
| clearIBC | Idris.AbsSyntax |
| clear_totcheck | Idris.AbsSyntax |
| Client | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| closeBlock | Idris.ParseHelpers, Idris.Parser |
| closure | IRTS.Java.ASTBuilding |
| CmdArg | Idris.Help |
| cmdOptType | Idris.AbsSyntax |
| codata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegen | Idris.AbsSyntax |
| codegenC | IRTS.CodegenC |
| codegenJava | IRTS.CodegenJava |
| codegenJavaScript | IRTS.CodegenJavaScript |
| codegenLLVM | Util.LLVMStubs |
| codegen_ | Idris.Parser |
| Coinductive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| collapse | Idris.Coverage |
| collapse' | Idris.Coverage |
| collapseCons | Idris.DataOpts |
| collapseNothing | Idris.Coverage |
| collapsible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| collect | Idris.ParseHelpers, Idris.Parser |
| collectDeferred | Idris.ElabTerm |
| colon | Util.Pretty |
| colour | Idris.Colours |
| ColourArg | Idris.Help |
| colourise | Idris.AbsSyntax |
| colouriseBound | Idris.Colours |
| colouriseData | Idris.Colours |
| colouriseFun | Idris.Colours |
| colouriseImplicit | Idris.Colours |
| colouriseKwd | Idris.Colours |
| colourisePrompt | Idris.Colours |
| colouriseType | Idris.Colours |
| ColourOff | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ColourOn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ColourREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ColourTheme | |
| 1 (Type/Class) | Idris.Colours |
| 2 (Data Constructor) | Idris.Colours |
| ColourType | Idris.Colours |
| columnNum | Idris.ParseHelpers, Idris.Parser |
| comma | Util.Pretty |
| Command | |
| 1 (Type/Class) | Core.Elaborate |
| 2 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Compile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compile | IRTS.Compiler |
| compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CompileTime | Core.CaseTree |
| CompleteFill | Core.ProofState, Core.Elaborate |
| complete_fill | Core.Elaborate |
| comprehension | Idris.ParseExpr, Idris.Parser |
| Compute | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compute | Core.Elaborate |
| ComputeLet | Core.ProofState, Core.Elaborate |
| computeLet | Core.Elaborate |
| ConCase | Core.CaseTree |
| conCase | IRTS.Bytecode |
| Const | Core.TT |
| constAlt | IRTS.Bytecode |
| Constant | Core.TT |
| constant | Idris.ParseExpr, Idris.Parser |
| CONSTCASE | IRTS.Bytecode |
| ConstCase | Core.CaseTree |
| constCase | IRTS.Bytecode |
| Constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraintArg | Idris.ParseExpr, Idris.Parser |
| constraintList | Idris.ParseExpr, Idris.Parser |
| constructor | Idris.ParseData, Idris.Parser |
| constType | IRTS.Java.JTypes |
| Context | Core.Evaluate |
| context | Core.ProofState, Core.Elaborate |
| contextArray | IRTS.Java.JTypes |
| contextParam | IRTS.Java.JTypes |
| convEq | Core.Evaluate |
| convEq' | Core.Evaluate |
| converts | Core.Typecheck |
| convertsC | Core.Typecheck |
| convSExp | Idris.IdeSlave |
| con_names | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| coverage | Idris.AbsSyntax |
| Ctxt | Core.TT |
| ctxtAlist | Core.Evaluate |
| DAlt | IRTS.Defunctionalise |
| DApp | IRTS.Defunctionalise |
| Data | Core.TT |
| DataColour | Idris.Colours |
| dataColour | Idris.Colours |
| DataDoc | Idris.Docs |
| dataI | Idris.ParseData, Idris.Parser |
| Datatype | Core.TT |
| data_ | Idris.ParseData, Idris.Parser |
| DbgLevel | IRTS.CodegenCommon |
| DC | IRTS.Defunctionalise |
| DCase | IRTS.Defunctionalise |
| DChkCase | IRTS.Defunctionalise |
| DCon | Core.TT |
| DConCase | IRTS.Defunctionalise |
| DConst | IRTS.Defunctionalise |
| DConstCase | IRTS.Defunctionalise |
| DConstructor | IRTS.Defunctionalise |
| DDecl | IRTS.Defunctionalise |
| DDefaultCase | IRTS.Defunctionalise |
| DDefs | IRTS.Defunctionalise |
| debind | Idris.DSL |
| debindApp | Idris.DSL |
| DEBUG | IRTS.CodegenCommon |
| DebugInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| decl | Idris.Parser |
| decl' | Idris.Parser |
| declare | IRTS.Defunctionalise |
| declared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| declareFinalObjectArray | IRTS.Java.ASTBuilding |
| declArgs | IRTS.Compiler |
| decorateid | Idris.ElabDecls |
| decoration | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Def | Core.Evaluate |
| defaultAlt | IRTS.Bytecode |
| DefaultCase | Core.CaseTree |
| defaultOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DefaultPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultPkg | Pkg.PParser |
| defaultSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultTheme | Idris.Colours |
| DefaultTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| default_access | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| default_total | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Defer | Core.ProofState, Core.Elaborate |
| defer | Core.Elaborate |
| deferred | Core.ProofState, Core.Elaborate |
| DeferType | Core.ProofState, Core.Elaborate |
| deferType | Core.Elaborate |
| defer_totcheck | Idris.AbsSyntax |
| defined | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Defn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defunctionalise | IRTS.Defunctionalise |
| delab | Idris.Delaborate |
| delab' | Idris.Delaborate |
| delabTy | Idris.Delaborate |
| delabTy' | Idris.Delaborate |
| DError | IRTS.Defunctionalise |
| desugar | Idris.DSL |
| DExp | IRTS.Defunctionalise |
| DForeign | IRTS.Defunctionalise |
| DFun | IRTS.Defunctionalise |
| Dictionary | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dictionary | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| directive | Idris.Parser |
| disallowImp | Idris.ParseExpr, Idris.Parser |
| discard | Core.TT |
| displayHelp | Idris.REPL |
| DLet | IRTS.Defunctionalise |
| DNothing | IRTS.Defunctionalise |
| DoBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DoBindP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| doBlock | Idris.ParseExpr, Idris.Parser |
| Doc | |
| 1 (Type/Class) | Util.Pretty |
| 2 (Type/Class) | Idris.Docs |
| 3 (Data Constructor) | Idris.Docs |
| docClass | Idris.Docs |
| docComment | Idris.ParseHelpers, Idris.Parser |
| docData | Idris.Docs |
| docFun | Idris.Docs |
| DocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DoExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DoLet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DoLetP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| done | Core.ProofState, Core.Elaborate |
| dontunify | Core.ProofState, Core.Elaborate |
| DOp | IRTS.Defunctionalise |
| DoProofSearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| double | Util.Pretty |
| doubleQuotes | Util.Pretty |
| doubleType | IRTS.Java.JTypes |
| do_ | Idris.ParseExpr, Idris.Parser |
| DProj | IRTS.Defunctionalise |
| dropGiven | Core.ProofState, Core.Elaborate |
| DSL | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl | Idris.ParseData, Idris.Parser |
| DSL' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_apply | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_bind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_info | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_lambda | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_let | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_pure | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_return | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dsl_var | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dumpBC | IRTS.DumpBC |
| DumpCases | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dumpDecl | Idris.AbsSyntax |
| dumpDecls | Idris.AbsSyntax |
| DumpDefun | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dumpDefuns | IRTS.Defunctionalise |
| dumpInstance | Idris.REPL |
| dumpMethod | Idris.REPL |
| dumpprobs | Core.Elaborate |
| dumpState | Idris.Prover |
| DUpdate | IRTS.Defunctionalise |
| DV | IRTS.Defunctionalise |
| Dynamic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DynamicLib | Util.DynamicLinker |
| DynamicLink | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_cons | |
| 1 (Function) | Core.TT |
| 2 (Function) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_tcon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_type | Core.TT |
| d_typename | Core.TT |
| d_typetag | Core.TT |
| EA | Idris.ElabDecls |
| EAll | Idris.ElabDecls |
| EDefns | Idris.ElabDecls |
| Edit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| edit | Idris.REPL |
| eEVAL | IRTS.Defunctionalise |
| EInfo | Idris.ElabTerm |
| EitherErr | Idris.AbsSyntax |
| Elab | Core.Elaborate |
| elab | Idris.ElabTerm |
| Elab' | Core.Elaborate |
| elabCaseBlock | Idris.ElabDecls |
| elabClass | Idris.ElabDecls |
| elabClause | Idris.ElabDecls |
| elabClauses | Idris.ElabDecls |
| elabCon | Idris.ElabDecls |
| ElabD | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elabData | Idris.ElabDecls |
| elabDecl | Idris.ElabDecls |
| elabDecl' | Idris.ElabDecls |
| elabDecls | Idris.ElabDecls |
| ElabInfo | Idris.ElabTerm |
| elabInstance | Idris.ElabDecls |
| elaborate | Core.Elaborate |
| Elaborating | Core.TT |
| elabPE | Idris.ElabDecls |
| elabPostulate | Idris.ElabDecls |
| elabPrims | Idris.ElabDecls |
| elabProvider | Idris.ElabDecls |
| elabRecord | Idris.ElabDecls |
| ElabState | Core.Elaborate |
| elabStep | Idris.Prover |
| elabTransform | Idris.ElabDecls |
| elabType | Idris.ElabDecls |
| elabType' | Idris.ElabDecls |
| elabVal | Idris.ElabDecls |
| elabValBind | Idris.ElabDecls |
| ElabWhat | Idris.ElabDecls |
| elog | Core.Elaborate |
| empty | Util.Pretty |
| emptyContext | Core.TT |
| emptyFC | Core.TT |
| EndUnify | Core.ProofState, Core.Elaborate |
| end_unify | Core.Elaborate |
| Env | Core.TT |
| envAtFocus | Core.ProofState, Core.Elaborate |
| environment | IRTS.CodegenCommon |
| envlen | Core.TT |
| EnvTT | Core.TT |
| envTupleType | Idris.ElabTerm |
| eol | Idris.ParseHelpers, Idris.Parser |
| eqCon | Idris.AbsSyntax |
| eqDecl | Idris.AbsSyntax |
| eqProp | Idris.ParseHelpers, Idris.Parser |
| eqTy | Idris.AbsSyntax |
| equals | Util.Pretty |
| Equiv | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| equiv | Core.Elaborate |
| Erased | Core.TT |
| Err | Core.TT |
| errAt | Core.Elaborate |
| ErrContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| errContext | Idris.AbsSyntax |
| errEnv | Core.Typecheck |
| errLine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ERROR | IRTS.Bytecode |
| Error | Core.TT |
| ErrorReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| erun | Core.Elaborate |
| ES | Core.Elaborate |
| ETypes | Idris.ElabDecls |
| Eval | |
| 1 (Data Constructor) | Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EvalApply | IRTS.Defunctionalise |
| EvalCase | IRTS.Defunctionalise |
| evalD | IRTS.Inliner |
| EvalIn | Core.ProofState, Core.Elaborate |
| eval_in | Core.Elaborate |
| Exact | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| exact | Core.Elaborate |
| exceptionType | IRTS.Java.JTypes |
| execElab | Core.Elaborate |
| execout | Pkg.PParser |
| execScript | Idris.REPL |
| Executable | IRTS.CodegenCommon |
| Execute | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| execute | Core.Execute |
| ExecVal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| existsCon | Idris.AbsSyntax |
| Exp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expandDo | Idris.DSL |
| ExpandLet | Core.ProofState, Core.Elaborate |
| expandLet | Core.Elaborate |
| expandNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expandParams | Idris.AbsSyntax |
| expandParamsD | Idris.AbsSyntax |
| expl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ExplicitD | Idris.PartialEval |
| explicitNames | Core.TT |
| ExplicitS | Idris.PartialEval |
| expl_param | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Expr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expr | Idris.ParseExpr, Idris.Parser |
| expr' | Idris.ParseExpr, Idris.Parser |
| ExprArg | Idris.Help |
| extendWithNull | IRTS.Java.ASTBuilding |
| Extension | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| extension | Idris.ParseExpr, Idris.Parser |
| extensions | Idris.ParseExpr, Idris.Parser |
| externalExpr | Idris.ParseExpr, Idris.Parser |
| extraHelp | Idris.Help |
| Fails | Core.Unify |
| falseDecl | Idris.AbsSyntax |
| falseTy | Idris.AbsSyntax |
| FAny | IRTS.Lang, IRTS.Defunctionalise |
| FArith | IRTS.Lang, IRTS.Defunctionalise |
| FC | |
| 1 (Type/Class) | Core.TT |
| 2 (Data Constructor) | Core.TT |
| FC' | |
| 1 (Type/Class) | Core.TT |
| 2 (Data Constructor) | Core.TT |
| FCallType | IRTS.Lang, IRTS.Defunctionalise |
| fcat | Util.Pretty |
| FConstructor | IRTS.Lang, IRTS.Defunctionalise |
| fc_column | Core.TT |
| fc_fname | Core.TT |
| fc_line | Core.TT |
| FFunction | IRTS.Lang, IRTS.Defunctionalise |
| FFunctionIO | IRTS.Lang, IRTS.Defunctionalise |
| FileArg | Idris.Help |
| fileFC | Core.TT |
| Filename | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fileName | Idris.ParseHelpers, Idris.Parser |
| Fill | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fill | Core.Elaborate |
| finalise | Core.TT |
| findCalls | Core.CaseTree |
| findFC | Idris.Parser |
| findImport | Idris.Imports |
| findInPath | Idris.Imports |
| findInstances | Idris.ElabTerm |
| findStatics | Idris.AbsSyntax |
| findUnusedArgs | Idris.UnusedArgs |
| findUsedArgs | Core.CaseTree |
| first | Util.Pretty |
| Fix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixColour | Idris.REPL |
| FixDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixErrorMsg | Idris.ParseHelpers, Idris.Parser |
| Fixity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixity | Idris.ParseOps, Idris.Parser |
| fixityType | Idris.ParseOps, Idris.Parser |
| Fl | Core.TT |
| FLang | IRTS.Lang, IRTS.Defunctionalise |
| float | |
| 1 (Function) | Util.Pretty |
| 2 (Function) | Idris.ParseHelpers, Idris.Parser |
| fmapMB | Core.TT |
| FnCase | Core.CaseTree |
| fnDecl | Idris.Parser |
| fnDecl' | Idris.Parser |
| fnName | Idris.ParseOps, Idris.Parser |
| FnOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| FnOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fnOpts | Idris.Parser |
| fnub | Idris.Coverage |
| fnub' | Idris.Coverage |
| FObject | IRTS.Lang, IRTS.Defunctionalise |
| Focus | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| focus | Core.Elaborate |
| Forall | Core.ProofState, Core.Elaborate |
| forall | Core.Elaborate |
| forceable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| forceArgs | Idris.DataOpts |
| forCodegen | Idris.AbsSyntax |
| FOREIGNCALL | IRTS.Bytecode |
| foreignType | IRTS.Java.JTypes |
| foreignWrapperType | IRTS.Java.JTypes |
| forget | Core.TT |
| Forgot | Core.TT |
| FPtr | IRTS.Lang, IRTS.Defunctionalise |
| freeNames | Core.TT |
| Frozen | Core.Evaluate |
| fsep | Util.Pretty |
| FStatic | IRTS.Lang, IRTS.Defunctionalise |
| FString | IRTS.Lang, IRTS.Defunctionalise |
| FType | IRTS.Lang, IRTS.Defunctionalise |
| fullExpr | Idris.ParseExpr, Idris.Parser |
| fullRender | Util.Pretty |
| fullTactic | Idris.ParseExpr, Idris.Parser |
| Function | Core.Evaluate |
| FunctionColour | Idris.Colours |
| functionColour | Idris.Colours |
| FunDoc | |
| 1 (Data Constructor) | Idris.Docs |
| 2 (Type/Class) | Idris.Docs |
| FUnit | IRTS.Lang, IRTS.Defunctionalise |
| GD | Core.ProofState, Core.Elaborate |
| genAll | Idris.Coverage |
| genArgs | IRTS.Defunctionalise |
| genClauses | Idris.Coverage |
| getAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getAllNames | Idris.AbsSyntax |
| getArgTys | Core.TT |
| getAux | Core.Elaborate |
| getBC | Idris.REPL |
| getBinDir | Paths_idris |
| getCC | Util.System |
| getClause | Idris.CaseSplit |
| getCmdLine | Idris.AbsSyntax |
| getCodegen | Idris.REPL |
| getCoercionsTo | Idris.AbsSyntax |
| getColour | Idris.REPL |
| getConsts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getContext | Idris.AbsSyntax |
| getCPU | Idris.REPL |
| getDataDir | Paths_idris |
| getDataFileName | Paths_idris |
| getDefaultTargetTriple | Util.LLVMStubs |
| getDocs | Idris.Docs |
| getDumpCases | Idris.AbsSyntax |
| getDumpDefun | Idris.AbsSyntax |
| getErrColumn | Idris.Error |
| getErrLine | Idris.Error |
| getExecScript | Idris.REPL |
| getExecutablePom | Util.System |
| getExps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getFargpos | Idris.UnusedArgs |
| getFC | Idris.ParseHelpers, Idris.Parser |
| getFile | Idris.REPL |
| getFlags | Idris.AbsSyntax |
| getFn | IRTS.Defunctionalise |
| getFTypes | IRTS.Compiler |
| getHdrs | Idris.AbsSyntax |
| getHostCPUName | Util.LLVMStubs |
| getIBCSubDir | Idris.REPL |
| getIdrisLibDir | Util.System |
| getIdrisUserDataDir | Idris.REPL |
| getImportDir | Idris.REPL |
| getImps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getIncFlags | Util.System |
| getInferTerm | Idris.AbsSyntax |
| getInferType | Idris.AbsSyntax |
| getInitScript | Idris.REPL |
| getInternalApp | Idris.AbsSyntax |
| getIState | Idris.AbsSyntax |
| getLanguageExt | Idris.REPL |
| getLibDir | Paths_idris |
| getLibexecDir | Paths_idris |
| getLibFlags | Util.System |
| getLibs | Idris.AbsSyntax |
| getLog | Core.Elaborate |
| getModuleFiles | Idris.Chaser |
| getMvn | Util.System |
| getName | Idris.AbsSyntax |
| getNextName | IRTS.Lang, IRTS.Defunctionalise |
| getNoBanner | Idris.AbsSyntax |
| getObjectFiles | Idris.AbsSyntax |
| getOptLevel | Idris.REPL |
| getOutput | Idris.REPL |
| getOutputTy | Idris.REPL |
| getPArity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getPBtys | Idris.ElabDecls |
| getPkg | Idris.REPL |
| getPkgClean | Idris.REPL |
| getPkgDir | Idris.REPL |
| getPrim | IRTS.Compiler |
| getPriority | Idris.AbsSyntax |
| getProofClause | Idris.CaseSplit |
| getProvided | Idris.Providers |
| getQuiet | Idris.AbsSyntax |
| getRetTy | Core.TT |
| getScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getSO | Idris.AbsSyntax |
| getSpecApps | Idris.PartialEval |
| getSysconfDir | Paths_idris |
| getTargetDir | Util.System |
| getTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getTotality | Idris.AbsSyntax |
| getTriple | Idris.REPL |
| getUniq | Idris.CaseSplit |
| get_context | Core.Elaborate |
| get_deferred | Core.Elaborate |
| get_env | Core.Elaborate |
| get_guess | Core.Elaborate |
| get_holes | Core.Elaborate |
| get_instances | Core.Elaborate |
| get_probs | Core.Elaborate |
| get_term | Core.Elaborate |
| get_type | Core.Elaborate |
| get_type_val | Core.Elaborate |
| GHole | Core.TT |
| Glob | IRTS.Lang, IRTS.Defunctionalise |
| globalContext | IRTS.Java.JTypes |
| globalContextID | IRTS.Java.JTypes |
| Goal | Core.ProofState, Core.Elaborate |
| goal | Core.Elaborate |
| goalAtFocus | Core.ProofState, Core.Elaborate |
| GoalType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| goalType | Core.ProofState, Core.Elaborate |
| groupsOf | IRTS.Defunctionalise |
| gteProp | Idris.ParseHelpers, Idris.Parser |
| gtProp | Idris.ParseHelpers, Idris.Parser |
| Guess | Core.TT |
| hang | Util.Pretty |
| hcat | Util.Pretty |
| Help | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| help | Idris.Help |
| helphead | Idris.REPL |
| Hidden | Core.Evaluate |
| hide_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| HNF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| hnf | Core.Evaluate |
| HNF_Compute | Core.ProofState, Core.Elaborate |
| hnf_compute | Core.Elaborate |
| Hole | Core.TT |
| holes | Core.ProofState, Core.Elaborate |
| hsep | Util.Pretty |
| hsimpleExpr | Idris.ParseExpr, Idris.Parser |
| hvar | IRTS.Simplified |
| I | Core.TT |
| IA | Idris.ElabDecls |
| IBC | Idris.Imports |
| ibc | Idris.IBC |
| IBCAccess | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCCG | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCCGFlag | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCCoercion | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCData | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCDyLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFile | |
| 1 (Type/Class) | Idris.IBC |
| 2 (Data Constructor) | Idris.IBC |
| IBCFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFlags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCHeader | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCKeyword | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCLineApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCObj | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ibcPath | Idris.Imports |
| ibcPathNoFallback | Idris.Imports |
| ibcPathWithFallback | Idris.Imports |
| IBCStatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCSubDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTrans | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ibcVersion | Idris.IBC |
| IBCWrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ibc_access | Idris.IBC |
| ibc_cg | Idris.IBC |
| ibc_cgflags | Idris.IBC |
| ibc_classes | Idris.IBC |
| ibc_coercions | Idris.IBC |
| ibc_datatypes | Idris.IBC |
| ibc_defs | Idris.IBC |
| ibc_docstrings | Idris.IBC |
| ibc_dsls | Idris.IBC |
| ibc_dynamic_libs | Idris.IBC |
| ibc_fixes | Idris.IBC |
| ibc_flags | Idris.IBC |
| ibc_hdrs | Idris.IBC |
| ibc_implicits | Idris.IBC |
| ibc_imports | Idris.IBC |
| ibc_instances | Idris.IBC |
| ibc_keywords | Idris.IBC |
| ibc_libs | Idris.IBC |
| ibc_lineapps | Idris.IBC |
| ibc_objs | Idris.IBC |
| ibc_optimise | Idris.IBC |
| ibc_statics | Idris.IBC |
| ibc_syntax | Idris.IBC |
| ibc_total | Idris.IBC |
| ibc_transforms | Idris.IBC |
| ibc_write | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| identifier | Idris.ParseHelpers, Idris.Parser |
| IdeSlave | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ideslave | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ideslave | Idris.REPL |
| IdeSlaveCommand | Idris.IdeSlave |
| ideslaveProcess | Idris.REPL |
| ideslavePutSExp | Idris.AbsSyntax |
| ideslaveStart | Idris.REPL |
| idiom | Idris.ParseExpr, Idris.Parser |
| IDR | Idris.Imports |
| Idris | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris | Idris.REPL |
| idrisCatch | Idris.Error |
| idrisClosureType | IRTS.Java.JTypes |
| IdrisColour | |
| 1 (Type/Class) | Idris.Colours |
| 2 (Data Constructor) | Idris.Colours |
| idrisInit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdrisInnerParser | |
| 1 (Type/Class) | Idris.ParseHelpers, Idris.Parser |
| 2 (Data Constructor) | Idris.ParseHelpers, Idris.Parser |
| idrisMain | Idris.REPL |
| idrisObjectType | IRTS.Java.JTypes |
| IdrisParser | Idris.ParseHelpers, Idris.Parser |
| idrisStyle | Idris.ParseHelpers, Idris.Parser |
| idrisTailCallClosureType | IRTS.Java.JTypes |
| idris_calledgraph | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_callgraph | 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_constraints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_datatypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_defertotcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_docstrings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_dsls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_dynamic_libs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_flags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_hdrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_implicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_infixes | 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 | Pkg.PParser |
| idris_metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_objs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_optimisation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_options | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_opts | Pkg.PParser |
| idris_outh | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_outputmode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_patdefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_scprims | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_statics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_totcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_transforms | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ierror | Idris.Error |
| ifail | Idris.Error |
| IFileType | Idris.Imports |
| ihPrintError | Idris.AbsSyntax |
| ihPrintResult | Idris.AbsSyntax |
| ihputStrLn | Idris.AbsSyntax |
| ihWarn | Idris.AbsSyntax |
| iLOG | Idris.AbsSyntax |
| Imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| impl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Implicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| implicit | Idris.AbsSyntax |
| implicit' | Idris.AbsSyntax |
| implicitable | Core.TT |
| implicitAllowed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| implicitArg | Idris.ParseExpr, Idris.Parser |
| ImplicitColour | Idris.Colours |
| implicitColour | Idris.Colours |
| ImplicitD | Idris.PartialEval |
| implicitise | Idris.AbsSyntax |
| ImplicitS | Idris.PartialEval |
| ImportDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| import_ | Idris.Parser |
| Impossible | Core.TT |
| ImpossibleCase | Core.CaseTree |
| impShow | Idris.AbsSyntax |
| Inaccessible | Core.TT |
| iName | Idris.ParseHelpers, Idris.Parser |
| inblock | Idris.ElabTerm |
| IncompleteTerm | Core.TT |
| indent | |
| 1 (Function) | Idris.ParseHelpers, Idris.Parser |
| 2 (Function) | IRTS.DumpBC |
| indented | |
| 1 (Function) | Idris.Delaborate |
| 2 (Function) | Idris.ParseHelpers, Idris.Parser |
| indentedBlock | Idris.ParseHelpers, Idris.Parser |
| indentedBlock1 | Idris.ParseHelpers, Idris.Parser |
| indentedBlockS | Idris.ParseHelpers, Idris.Parser |
| IndentProperty | |
| 1 (Type/Class) | Idris.ParseHelpers, Idris.Parser |
| 2 (Data Constructor) | Idris.ParseHelpers, Idris.Parser |
| indentPropHolds | Idris.ParseHelpers, Idris.Parser |
| indent_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| index_first | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| index_next | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferCon | Idris.AbsSyntax |
| inferDecl | Idris.AbsSyntax |
| inferredDiff | Idris.ElabDecls |
| inferTy | Idris.AbsSyntax |
| InfiniteUnify | Core.TT |
| Infixl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InfixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Infixr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Info | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infP | Idris.AbsSyntax |
| infTerm | Idris.AbsSyntax |
| initContext | Core.Evaluate |
| initDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initElaborator | Core.Elaborate |
| initEval | Core.Evaluate |
| initIBC | Idris.IBC |
| initScript | Idris.REPL |
| initsEndAt | Idris.ParseHelpers, Idris.Parser |
| injective | Core.ProofState, Core.Elaborate |
| inl | IRTS.Inliner |
| Inlinable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inlinable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Inline | IRTS.Lang, IRTS.Defunctionalise |
| inline | IRTS.Inliner |
| inlineDef | Idris.Inliner |
| inlineTerm | Idris.Inliner |
| inPattern | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| insertScript | Idris.REPL |
| installIBC | Pkg.Package |
| installObj | Pkg.Package |
| installPkg | Pkg.Package |
| Instance | Core.ProofState, Core.Elaborate |
| instanceArg | Core.Elaborate |
| InstanceN | Core.TT |
| instanceName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| instances | Core.ProofState, Core.Elaborate |
| instance_ | Idris.Parser |
| instantiate | Core.TT |
| int | Util.Pretty |
| integer | |
| 1 (Function) | Util.Pretty |
| 2 (Function) | Idris.ParseHelpers, Idris.Parser |
| IntegerAtom | Idris.IdeSlave |
| integerType | IRTS.Java.JTypes |
| interMap | IRTS.DumpBC |
| internalExpr | Idris.ParseExpr, Idris.Parser |
| InternalMsg | Core.TT |
| Interpret | Idris.IdeSlave |
| InterpretScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Intro | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| intro | Core.Elaborate |
| Intros | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IntroTy | Core.ProofState, Core.Elaborate |
| introTy | Core.Elaborate |
| IntTy | Core.TT |
| intTyToJType | IRTS.Java.JTypes |
| intTyWidth | Core.TT |
| InvocationTarget | IRTS.Java.ASTBuilding |
| IOption | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| iPrintError | Idris.AbsSyntax |
| iPrintResult | Idris.AbsSyntax |
| iputGoal | Idris.AbsSyntax |
| iputStrLn | Idris.AbsSyntax |
| ir | IRTS.Compiler |
| irMain | IRTS.Compiler |
| isArray | IRTS.Java.JTypes |
| isCon | IRTS.Compiler |
| isConName | Core.Evaluate |
| isConst | IRTS.Bytecode |
| isDConName | Core.Evaluate |
| isDocCommentMarker | Idris.ParseHelpers, Idris.Parser |
| isEmpty | Util.Pretty |
| isEol | Idris.ParseHelpers, Idris.Parser |
| isetPrompt | Idris.AbsSyntax |
| isFloating | IRTS.Java.JTypes |
| isFnName | Core.Evaluate |
| isInjective | Core.TT |
| isnewtype | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isPrimitive | IRTS.Java.JTypes |
| isString | IRTS.Java.JTypes |
| IState | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isTConName | Core.Evaluate |
| isType | Core.Typecheck |
| isUndefined | Idris.AbsSyntax |
| IT16 | Core.TT |
| IT32 | Core.TT |
| IT64 | Core.TT |
| IT8 | Core.TT |
| italic | Idris.Colours |
| ITBig | Core.TT |
| itBitsName | Core.TT |
| ITChar | Core.TT |
| ITFixed | Core.TT |
| ITNative | Core.TT |
| Itself | Core.Evaluate |
| ITVec | Core.TT |
| iucheck | Idris.Error |
| iWarn | Idris.AbsSyntax |
| JavaScript | IRTS.CodegenJavaScript |
| jConst | IRTS.Java.ASTBuilding |
| jInt | IRTS.Java.ASTBuilding |
| jName | IRTS.Java.ASTBuilding |
| jReturn | IRTS.Java.ASTBuilding |
| JSTarget | IRTS.CodegenJavaScript |
| jString | IRTS.Java.ASTBuilding |
| keepGiven | Core.ProofState, Core.Elaborate |
| keepTerminator | Idris.ParseHelpers, Idris.Parser |
| Keyword | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| KeywordColour | Idris.Colours |
| keywordColour | Idris.Colours |
| L | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | IRTS.Bytecode |
| LAlt | IRTS.Lang, IRTS.Defunctionalise |
| Lam | Core.TT |
| lambda | Idris.ParseExpr, Idris.Parser |
| lambdaLift | IRTS.Lang, IRTS.Defunctionalise |
| LAnd | IRTS.Lang, IRTS.Defunctionalise |
| LanguageExt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LANG_C | IRTS.Lang, IRTS.Defunctionalise |
| LANG_JAVA | IRTS.Lang, IRTS.Defunctionalise |
| LApp | IRTS.Lang, IRTS.Defunctionalise |
| LASHR | IRTS.Lang, IRTS.Defunctionalise |
| lastIndent | Idris.ParseHelpers, Idris.Parser |
| lastParse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| lazyarg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LBitCast | IRTS.Lang, IRTS.Defunctionalise |
| lbrace | Util.Pretty |
| lbrack | Util.Pretty |
| LCase | IRTS.Lang, IRTS.Defunctionalise |
| lchar | Idris.ParseHelpers, Idris.Parser |
| LChInt | IRTS.Lang, IRTS.Defunctionalise |
| LCompl | IRTS.Lang, IRTS.Defunctionalise |
| LCon | IRTS.Lang, IRTS.Defunctionalise |
| LConCase | IRTS.Lang, IRTS.Defunctionalise |
| LConst | IRTS.Lang, IRTS.Defunctionalise |
| LConstCase | IRTS.Lang, IRTS.Defunctionalise |
| LConstructor | IRTS.Lang, IRTS.Defunctionalise |
| LDecl | IRTS.Lang, IRTS.Defunctionalise |
| LDefaultCase | IRTS.Lang, IRTS.Defunctionalise |
| LDefs | IRTS.Lang, IRTS.Defunctionalise |
| ldefs | IRTS.Simplified |
| LeftErr | Idris.AbsSyntax |
| LeftMode | Util.Pretty |
| LEq | IRTS.Lang, IRTS.Defunctionalise |
| LError | IRTS.Lang, IRTS.Defunctionalise |
| Let | Core.TT |
| LetBind | Core.ProofState, Core.Elaborate |
| letbind | Core.Elaborate |
| LetTac | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LetTacTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| let_ | Idris.ParseExpr, Idris.Parser |
| LExp | IRTS.Lang, IRTS.Defunctionalise |
| LFACos | IRTS.Lang, IRTS.Defunctionalise |
| LFASin | IRTS.Lang, IRTS.Defunctionalise |
| LFATan | IRTS.Lang, IRTS.Defunctionalise |
| LFCeil | IRTS.Lang, IRTS.Defunctionalise |
| LFCos | IRTS.Lang, IRTS.Defunctionalise |
| LFExp | IRTS.Lang, IRTS.Defunctionalise |
| LFFloor | IRTS.Lang, IRTS.Defunctionalise |
| LFloatInt | IRTS.Lang, IRTS.Defunctionalise |
| LFloatStr | IRTS.Lang, IRTS.Defunctionalise |
| LFLog | IRTS.Lang, IRTS.Defunctionalise |
| LForce | IRTS.Lang, IRTS.Defunctionalise |
| LForeign | IRTS.Lang, IRTS.Defunctionalise |
| LFork | IRTS.Lang, IRTS.Defunctionalise |
| LFSin | IRTS.Lang, IRTS.Defunctionalise |
| LFSqrt | IRTS.Lang, IRTS.Defunctionalise |
| LFTan | IRTS.Lang, IRTS.Defunctionalise |
| LFun | IRTS.Lang, IRTS.Defunctionalise |
| LGe | IRTS.Lang, IRTS.Defunctionalise |
| LGt | IRTS.Lang, IRTS.Defunctionalise |
| Lib | Util.DynamicLinker |
| libdeps | Pkg.PParser |
| lib_handle | Util.DynamicLinker |
| lib_name | Util.DynamicLinker |
| LIDR | Idris.Imports |
| LIdxVec | IRTS.Lang, IRTS.Defunctionalise |
| lift | IRTS.Lang, IRTS.Defunctionalise |
| liftAll | IRTS.Lang, IRTS.Defunctionalise |
| lifte | Idris.Prover |
| liftname | Idris.ElabTerm |
| liftParsed | IRTS.Java.Mangling |
| LiftState | IRTS.Lang, IRTS.Defunctionalise |
| lineLength | Util.Pretty |
| lineNum | Idris.ParseHelpers, Idris.Parser |
| LIntCh | IRTS.Lang, IRTS.Defunctionalise |
| LIntFloat | IRTS.Lang, IRTS.Defunctionalise |
| LIntStr | IRTS.Lang, IRTS.Defunctionalise |
| ListDynamic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| listenOnLocalhost | Util.Net |
| listExpr | Idris.ParseExpr, Idris.Parser |
| lit | Idris.REPL |
| LLam | IRTS.Lang, IRTS.Defunctionalise |
| LLazyApp | IRTS.Lang, IRTS.Defunctionalise |
| LLazyExp | IRTS.Lang, IRTS.Defunctionalise |
| LLe | IRTS.Lang, IRTS.Defunctionalise |
| LLet | IRTS.Lang, IRTS.Defunctionalise |
| LLSHR | IRTS.Lang, IRTS.Defunctionalise |
| LLt | IRTS.Lang, IRTS.Defunctionalise |
| LMinus | IRTS.Lang, IRTS.Defunctionalise |
| LMkVec | IRTS.Lang, IRTS.Defunctionalise |
| lname | IRTS.Lang, IRTS.Defunctionalise |
| LNoOp | IRTS.Lang, IRTS.Defunctionalise |
| LNothing | IRTS.Lang, IRTS.Defunctionalise |
| LNullPtr | IRTS.Lang, IRTS.Defunctionalise |
| Load | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LoadFile | Idris.IdeSlave |
| loadFromIFile | Idris.Parser |
| loadIBC | Idris.IBC |
| LoadingFailed | Core.TT |
| loadInputs | Idris.REPL |
| loadModule | Idris.Parser |
| loadModule' | Idris.Parser |
| loadSource | Idris.Parser |
| loadSource' | Idris.Parser |
| loadState | Core.Elaborate |
| Loc | IRTS.Lang, IRTS.Defunctionalise |
| localContext | IRTS.Java.JTypes |
| localContextID | IRTS.Java.JTypes |
| localVar | IRTS.Java.ASTBuilding |
| logLevel | Idris.AbsSyntax |
| LogLvl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| logLvl | Idris.AbsSyntax |
| longType | IRTS.Java.JTypes |
| lookAheadMatches | Idris.ParseHelpers, Idris.Parser |
| lookupCtxt | Core.TT |
| lookupCtxtExact | Core.TT |
| lookupCtxtName | Core.TT |
| lookupDef | Core.Evaluate |
| lookupDefAcc | Core.Evaluate |
| lookupNames | Core.Evaluate |
| lookupNameTotal | Core.Evaluate |
| lookupP | Core.Evaluate |
| lookupTotal | Core.Evaluate |
| lookupTy | Core.Evaluate |
| lookupTyEnv | Core.Evaluate |
| lookupVal | Core.Evaluate |
| LOp | IRTS.Lang, IRTS.Defunctionalise |
| LOpt | IRTS.Lang, IRTS.Defunctionalise |
| LOr | IRTS.Lang, IRTS.Defunctionalise |
| LPar | IRTS.Lang, IRTS.Defunctionalise |
| lparen | Util.Pretty |
| LPlus | IRTS.Lang, IRTS.Defunctionalise |
| LPrintNum | IRTS.Lang, IRTS.Defunctionalise |
| LPrintStr | IRTS.Lang, IRTS.Defunctionalise |
| LProj | IRTS.Lang, IRTS.Defunctionalise |
| LReadStr | IRTS.Lang, IRTS.Defunctionalise |
| LS | IRTS.Lang, IRTS.Defunctionalise |
| LSDiv | IRTS.Lang, IRTS.Defunctionalise |
| LSExt | IRTS.Lang, IRTS.Defunctionalise |
| LSGe | IRTS.Lang, IRTS.Defunctionalise |
| LSGt | IRTS.Lang, IRTS.Defunctionalise |
| LSHL | IRTS.Lang, IRTS.Defunctionalise |
| LSLe | IRTS.Lang, IRTS.Defunctionalise |
| LSLt | IRTS.Lang, IRTS.Defunctionalise |
| lsrcPath | Idris.Imports |
| LSRem | IRTS.Lang, IRTS.Defunctionalise |
| LStdErr | IRTS.Lang, IRTS.Defunctionalise |
| LStdIn | IRTS.Lang, IRTS.Defunctionalise |
| LStdOut | IRTS.Lang, IRTS.Defunctionalise |
| LStrConcat | IRTS.Lang, IRTS.Defunctionalise |
| LStrCons | IRTS.Lang, IRTS.Defunctionalise |
| LStrEq | IRTS.Lang, IRTS.Defunctionalise |
| LStrFloat | IRTS.Lang, IRTS.Defunctionalise |
| LStrHead | IRTS.Lang, IRTS.Defunctionalise |
| LStrIndex | IRTS.Lang, IRTS.Defunctionalise |
| LStrInt | IRTS.Lang, IRTS.Defunctionalise |
| LStrLen | IRTS.Lang, IRTS.Defunctionalise |
| LStrLt | IRTS.Lang, IRTS.Defunctionalise |
| LStrRev | IRTS.Lang, IRTS.Defunctionalise |
| LStrTail | IRTS.Lang, IRTS.Defunctionalise |
| lteProp | Idris.ParseHelpers, Idris.Parser |
| LTimes | IRTS.Lang, IRTS.Defunctionalise |
| ltProp | Idris.ParseHelpers, Idris.Parser |
| LTrunc | IRTS.Lang, IRTS.Defunctionalise |
| LUDiv | IRTS.Lang, IRTS.Defunctionalise |
| LUpdateVec | IRTS.Lang, IRTS.Defunctionalise |
| LURem | IRTS.Lang, IRTS.Defunctionalise |
| LV | IRTS.Lang, IRTS.Defunctionalise |
| LVar | IRTS.Lang, IRTS.Defunctionalise |
| lvar | IRTS.Simplified |
| LVMPtr | IRTS.Lang, IRTS.Defunctionalise |
| LXOr | IRTS.Lang, IRTS.Defunctionalise |
| LZExt | IRTS.Lang, IRTS.Defunctionalise |
| machine_inf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| main | Main |
| make | Pkg.Package |
| makefile | Pkg.PParser |
| MakeWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MakeWithBlock | Idris.IdeSlave |
| mangle | IRTS.Java.Mangling |
| mangle' | IRTS.Java.Mangling |
| mangleFull | IRTS.Java.Mangling |
| mangleWithPrefix | IRTS.Java.Mangling |
| mapPT | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapsnd | Idris.AbsSyntax |
| MArgTy | Idris.ElabDecls |
| matchApp | Idris.ParseExpr, Idris.Parser |
| matchClause | Idris.AbsSyntax |
| matchClause' | Idris.AbsSyntax |
| MatchFill | Core.ProofState, Core.Elaborate |
| MatchProblems | Core.ProofState, Core.Elaborate |
| matchProblems | Core.Elaborate |
| MatchRefine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| match_apply | Core.Elaborate |
| match_fill | Core.Elaborate |
| match_unify | Core.Unify |
| mathType | IRTS.Java.JTypes |
| MavenProject | IRTS.CodegenCommon |
| maybeWithNS | Idris.ParseHelpers, Idris.Parser |
| MetaVarArg | Idris.Help |
| Metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MethodN | Core.TT |
| methodsBlock | Idris.Parser |
| Missing | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mkApp | Core.TT |
| mkapp | IRTS.Simplified |
| mkApply | IRTS.Defunctionalise |
| mkApplyCase | IRTS.Defunctionalise |
| mkBigCase | IRTS.Defunctionalise |
| mkClassName | IRTS.Java.Mangling |
| MKCON | IRTS.Bytecode |
| mkDecls | IRTS.Compiler |
| mkDirCmd | Pkg.Package |
| mkEval | IRTS.Defunctionalise |
| mkfapp | IRTS.Simplified |
| mkFnCon | IRTS.Defunctionalise |
| mkIBC | Idris.IBC |
| mkIntIty | IRTS.Compiler |
| mkIty | IRTS.Compiler |
| mkIty' | IRTS.Compiler |
| mkLDecl | IRTS.Compiler |
| mkMultiPaths | Idris.Coverage |
| mkName | Idris.ParseHelpers, Idris.Parser |
| mkPApp | Idris.AbsSyntax |
| mkPatTm | Idris.Coverage |
| mkPE_TermDecl | Idris.PartialEval |
| mkPE_TyDecl | Idris.PartialEval |
| mkPrompt | Idris.REPL |
| mkSpecDecl | Idris.ElabTerm |
| mkSpecialised | Idris.ElabTerm |
| mkType | Idris.ParseExpr, Idris.Parser |
| mkUnderCon | IRTS.Defunctionalise |
| mkWith | Idris.CaseSplit |
| MN | Core.TT |
| Mode | Util.Pretty |
| mode | Util.Pretty |
| modifyConst | Idris.ParseExpr, Idris.Parser |
| ModImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ModuleArg | Idris.Help |
| moduleHeader | Idris.Parser |
| modules | Pkg.PParser |
| ModuleTree | Idris.Chaser |
| mod_deps | Idris.Chaser |
| mod_needsRecheck | Idris.Chaser |
| mod_path | Idris.Chaser |
| mod_time | Idris.Chaser |
| MonadicParsing | Idris.ParseHelpers, Idris.Parser |
| MoveLast | Core.ProofState, Core.Elaborate |
| movelast | Core.Elaborate |
| moveReg | IRTS.Bytecode |
| Msg | Core.TT |
| MTree | Idris.Chaser |
| multiLineComment | Idris.ParseHelpers, Idris.Parser |
| MultiPath | Idris.Coverage |
| Mutual | Core.Evaluate |
| mutual | Idris.Parser |
| Name | Core.TT |
| name | Idris.ParseHelpers, Idris.Parser |
| NameArg | Idris.Help |
| nameRoot | Idris.CaseSplit |
| namesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| namespace | |
| 1 (Function) | Idris.ElabTerm |
| 2 (Function) | Idris.Parser |
| namesUsed | Core.CaseTree |
| NameType | Core.TT |
| natcase | Idris.Transforms |
| NativeTy | Core.TT |
| nativeTyToJType | IRTS.Java.JTypes |
| nativeTyWidth | Core.TT |
| natTrans | Idris.Transforms |
| natural | Idris.ParseHelpers, Idris.Parser |
| NErased | Core.TT |
| nest | Util.Pretty |
| nestingSize | Util.Pretty |
| newContext | IRTS.Java.JTypes |
| newContextID | IRTS.Java.JTypes |
| newProof | Core.ProofState, Core.Elaborate |
| nextName | Core.TT |
| nextname | Core.ProofState, Core.Elaborate |
| next_tvar | Core.Evaluate |
| NLet | Core.TT |
| NoArg | Idris.Help |
| NoBanner | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoBasePkgs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoBuiltins | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoCoverage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Node | IRTS.CodegenJavaScript |
| noErrors | Idris.AbsSyntax |
| noImplicits | Idris.ParseExpr, Idris.Parser |
| NoInline | IRTS.Lang, IRTS.Defunctionalise |
| NonCollapsiblePostulate | Core.TT |
| NONE | IRTS.CodegenCommon |
| NonFunctionType | Core.TT |
| noOccurrence | Core.TT |
| NOP | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | IRTS.BCImp |
| noPartial | Idris.Coverage |
| NoPrelude | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoRewriting | Core.TT |
| normalise | Core.Evaluate |
| normaliseAll | Core.Evaluate |
| normaliseC | Core.Evaluate |
| normaliseTrace | Core.Evaluate |
| NoSuchVariable | Core.TT |
| NotCovering | Core.Evaluate |
| notEndApp | Idris.ParseHelpers, Idris.Parser |
| notEndBlock | Idris.ParseHelpers, Idris.Parser |
| NotInjective | Core.TT |
| notOpenBraces | Idris.ParseHelpers, Idris.Parser |
| NotPositive | Core.Evaluate |
| NotProductive | Core.Evaluate |
| notunified | Core.ProofState, Core.Elaborate |
| NoTypeDecl | Core.TT |
| no_errors | Core.Elaborate |
| no_imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NS | Core.TT |
| nsroot | Core.TT |
| NULL | IRTS.Bytecode |
| Object | IRTS.CodegenCommon |
| objectType | IRTS.Java.JTypes |
| objs | Pkg.PParser |
| OK | Core.TT |
| OLogging | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OneLineMode | Util.Pretty |
| OP | IRTS.Bytecode |
| opChars | Idris.ParseHelpers, Idris.Parser |
| openBlock | Idris.ParseHelpers, Idris.Parser |
| Operator | Core.Evaluate |
| operator | Idris.ParseHelpers, Idris.Parser |
| operatorFront | Idris.ParseOps, Idris.Parser |
| operatorLetter | Idris.ParseHelpers, Idris.Parser |
| opName | IRTS.Java.JTypes |
| Opt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt | Idris.REPL |
| Optimisable | Idris.DataOpts |
| Optimise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OptInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Option | Core.TT |
| OptionArg | Idris.Help |
| OptLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| optLevel | Idris.AbsSyntax |
| opt_cmdline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_coverage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_cpu | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_errContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_ibcsubdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_importdirs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_logLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_nobanner | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_optLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_outputTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_repl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_showimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_triple | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_typecase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_typeintype | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_verbose | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| orderPats | Core.TT |
| Other | Core.Evaluate |
| Output | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OutputMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OutputTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| outputTy | Idris.AbsSyntax |
| OutputType | IRTS.CodegenCommon |
| overload | Idris.ParseData, Idris.Parser |
| P | Core.TT |
| pAccess | Idris.IBC |
| PageMode | Util.Pretty |
| pairCon | Idris.AbsSyntax |
| pairDecl | Idris.AbsSyntax |
| pairTy | Idris.AbsSyntax |
| PAlternative | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAppBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| params | |
| 1 (Function) | Idris.ElabTerm |
| 2 (Function) | Idris.Parser |
| param_pos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parens | Util.Pretty |
| ParentN | Core.TT |
| PArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PArg' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pargdoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parseArgs | Idris.REPL |
| parseCmd | Idris.REPLParser |
| parseCodegen | Idris.REPL |
| parseDesc | Pkg.PParser |
| parseExpr | Idris.Parser |
| parseImports | Idris.Parser |
| parseMessage | Idris.IdeSlave |
| parseProg | Idris.Parser |
| parseTactic | Idris.Parser |
| Partial | Core.Evaluate |
| PartialFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| partial_eval | Idris.PartialEval |
| PatBind | Core.ProofState, Core.Elaborate |
| patbind | Core.Elaborate |
| Pattelab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pattern | Idris.Parser |
| PatternSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PatVar | Core.ProofState, Core.Elaborate |
| patvar | Core.Elaborate |
| pbinds | Idris.ElabDecls |
| pbty | Idris.ElabDecls |
| PCAF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pCG | Idris.IBC |
| pCGFlags | Idris.IBC |
| PClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pClasses | Idris.IBC |
| PClause | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pClause | Pkg.PParser |
| PClause' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PClauseR | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PClauses | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PCoerced | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pCoercions | Idris.IBC |
| pconst | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstant | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PData | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PData' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDatadecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDatatypes | Idris.IBC |
| PDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDecl' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDefs | Idris.IBC |
| PDirective | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDo' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDoBlock | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDocs | Idris.IBC |
| pdocstr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDSLs | Idris.IBC |
| pDyLibs | Idris.IBC |
| PEArgType | Idris.PartialEval |
| PElabError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PEq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pexp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PFalse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pFixes | Idris.IBC |
| pFlags | Idris.IBC |
| PGoal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Phase | Core.CaseTree |
| pHdrs | Idris.IBC |
| PHidden | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Pi | Core.TT |
| pi | Idris.ParseExpr, Idris.Parser |
| piBind | Idris.AbsSyntax |
| piBindp | Idris.AbsSyntax |
| PIdiom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pImports | Idris.IBC |
| PImpossible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pImps | Idris.IBC |
| PInferRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pInstances | Idris.IBC |
| pKeywords | Idris.IBC |
| Pkg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgBuild | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgClean | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgDesc | |
| 1 (Type/Class) | Pkg.PParser |
| 2 (Data Constructor) | Pkg.PParser |
| PkgInstall | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pkgname | Pkg.PParser |
| Placeholder | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PLam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLangExt | Idris.Parser |
| PLaterdecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| plazy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PLet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLibs | Idris.IBC |
| Plicity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLineApps | Idris.IBC |
| plog | Core.ProofState, Core.Elaborate |
| ploop | Idris.Prover |
| pmap | Core.TT |
| PMatchApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMutual | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PNamespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PNoImplicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pObjs | Idris.IBC |
| pomString | IRTS.Java.Pom |
| popIndent | Idris.ParseHelpers, Idris.Parser |
| pOptimise | Idris.IBC |
| postulate | Idris.Parser |
| PPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pparam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PParams | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PParser | Pkg.PParser |
| PPatvar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pPkg | Pkg.PParser |
| PPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProvider | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PReason | Core.Evaluate |
| prec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRecord | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prefix | Idris.ParseOps, Idris.Parser |
| prefixCallNamespaces | IRTS.Java.Mangling |
| PrefixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRefl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| premises | Core.ProofState, Core.Elaborate |
| prepare_apply | Core.Elaborate |
| PrepFill | Core.ProofState, Core.Elaborate |
| prep_fill | Core.Elaborate |
| PResolveTC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Pretty | Util.Pretty |
| pretty | Util.Pretty |
| prettyEnv | Core.TT |
| prettyImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PReturn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| previous | Core.ProofState, Core.Elaborate |
| PRewrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Prim | |
| 1 (Type/Class) | Idris.Primitives |
| 2 (Data Constructor) | Idris.Primitives |
| primDefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PrimFn | IRTS.Lang, IRTS.Defunctionalise |
| primFnType | IRTS.Java.JTypes |
| primitives | Idris.Primitives |
| primNames | Idris.AbsSyntax |
| Core.Elaborate | |
| priority | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| problems | Core.ProofState, Core.Elaborate |
| process | |
| 1 (Function) | Idris.IBC |
| 2 (Function) | Idris.REPL |
| processInput | Idris.REPL |
| processNetCmd | Idris.REPL |
| processTactic | Core.ProofState, Core.Elaborate |
| processTactic' | Core.Elaborate |
| Productive | Core.Evaluate |
| prog | Idris.Parser |
| ProgramLineComment | Core.TT |
| Proj | Core.TT |
| ProjCase | Core.CaseTree |
| PROJECT | IRTS.Bytecode |
| PROJECTINTO | IRTS.Bytecode |
| PromptColour | Idris.Colours |
| promptColour | Idris.Colours |
| proof | Core.Elaborate |
| proofExpr | Idris.ParseExpr, Idris.Parser |
| proofFail | Core.Elaborate |
| Proofs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofs | Idris.REPL |
| ProofSearch | |
| 1 (Data Constructor) | Idris.IdeSlave |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofSearch | Idris.ProofSearch |
| proofSearch' | Idris.ElabTerm |
| ProofSearchFail | Core.TT |
| ProofState | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Type/Class) | Core.ProofState, Core.Elaborate |
| 3 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofstate | Core.Elaborate |
| ProofTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proof_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Prove | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prove | Idris.Prover |
| prover | Idris.Prover |
| proverCompletion | Idris.Completion |
| proverSettings | Idris.Prover |
| provider | Idris.Parser |
| ProviderError | Core.TT |
| providerTy | Idris.Providers |
| pruneAlt | Idris.ElabTerm |
| pruneByType | Idris.ElabTerm |
| prunStateT | Core.Elaborate |
| PS | Core.ProofState, Core.Elaborate |
| pscript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pshow | Idris.Delaborate |
| psolve | Idris.ElabDecls |
| pstatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pStatics | Idris.IBC |
| PStr | Util.Pretty |
| PSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pSyntax | Idris.IBC |
| ptacimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTacImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTactic' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTactics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pterm | Core.ProofState, Core.Elaborate |
| ptext | Util.Pretty |
| pTotal | Idris.IBC |
| pToV | Core.TT |
| pToV' | Core.TT |
| pToVs | Core.TT |
| pTrans | Idris.IBC |
| PTransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PtrType | Core.TT |
| PTrue | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ptype | Core.ProofState, Core.Elaborate |
| PTyped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Public | Core.Evaluate |
| punctuate | Util.Pretty |
| PUnifyLog | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pureTerm | Core.TT |
| pushIndent | Idris.ParseHelpers, Idris.Parser |
| putIState | Idris.AbsSyntax |
| PVar | Core.TT |
| pvars | Idris.ElabDecls |
| PVTy | Core.TT |
| PWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PWithR | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| p_arity | Idris.Primitives |
| p_def | Idris.Primitives |
| p_lexp | Idris.Primitives |
| p_name | Idris.Primitives |
| p_total | Idris.Primitives |
| p_type | Idris.Primitives |
| QED | Core.ProofState, Core.Elaborate |
| Qed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| qed | Core.Elaborate |
| qelem | Idris.Coverage |
| qshow | Core.Elaborate |
| quickEq | Idris.Coverage |
| Quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quit | |
| 1 (Data Constructor) | Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quote | Core.Evaluate |
| quote | Core.Evaluate |
| quoteGoal | Idris.ParseExpr, Idris.Parser |
| quotes | Util.Pretty |
| RApp | Core.TT |
| rational | Util.Pretty |
| Raw | |
| 1 (Type/Class) | Core.TT |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| RawDatatype | Core.TT |
| RawFun | |
| 1 (Type/Class) | Core.TT |
| 2 (Data Constructor) | Core.TT |
| RawOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| raw_apply | Core.TT |
| raw_unapply | Core.TT |
| RBind | Core.TT |
| rbrace | Util.Pretty |
| rbrack | Util.Pretty |
| RConst | Core.TT |
| RConstant | Core.TT |
| RData | Core.TT |
| RDatatype | Core.TT |
| RDef | Core.TT |
| REBASE | IRTS.Bytecode |
| receiveInput | Idris.Prover |
| recheck | Core.Typecheck |
| recheckC | Idris.ElabDecls |
| record | Idris.ParseData, Idris.Parser |
| recordType | Idris.ParseExpr, Idris.Parser |
| recursive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reduceDoc | Util.Pretty |
| Ref | Core.TT |
| Refine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflCall | Idris.ElabTerm |
| Reflect | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflect | Idris.ElabTerm |
| reflectBinder | Idris.ElabTerm |
| reflectConstant | Idris.ElabTerm |
| reflectEnv | Idris.ElabTerm |
| reflectErr | Idris.ElabTerm |
| Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflectName | Idris.ElabTerm |
| reflectNameType | Idris.ElabTerm |
| reflectUExp | Idris.ElabTerm |
| reflm | Idris.ElabTerm |
| Reg | |
| 1 (Type/Class) | IRTS.BCImp |
| 2 (Type/Class) | IRTS.Bytecode |
| Regret | Core.ProofState, Core.Elaborate |
| regret | Core.Elaborate |
| reify | Idris.ElabTerm |
| reifyApp | Idris.ElabTerm |
| reifyRaw | Idris.ElabTerm |
| reifyRawApp | Idris.ElabTerm |
| reifyTT | Idris.ElabTerm |
| reifyTTApp | Idris.ElabTerm |
| reifyTTBinder | Idris.ElabTerm |
| reifyTTBinderApp | Idris.ElabTerm |
| reifyTTConst | Idris.ElabTerm |
| reifyTTConstApp | Idris.ElabTerm |
| reifyTTName | Idris.ElabTerm |
| reifyTTNameApp | Idris.ElabTerm |
| reifyTTNamespace | Idris.ElabTerm |
| reifyTTNameType | Idris.ElabTerm |
| reifyTTUExp | Idris.ElabTerm |
| Reload | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| removeProof | Idris.REPL |
| render | Util.Pretty |
| renderStyle | Util.Pretty |
| Reorder | Core.ProofState, Core.Elaborate |
| reorder_claims | Core.Elaborate |
| repl | Idris.REPL |
| replaceSplits | Idris.CaseSplit |
| replCompletion | Idris.Completion |
| REPLCompletions | Idris.IdeSlave |
| replSettings | Idris.REPL |
| report | Idris.Error |
| RESERVE | IRTS.Bytecode |
| reserved | Idris.ParseHelpers, Idris.Parser |
| reservedOp | Idris.ParseHelpers, Idris.Parser |
| resolveProof | Idris.REPL |
| resolveTC | Idris.ElabTerm |
| Rewrite | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| rewrite | Core.Elaborate |
| rewriteTerm | Idris.ParseExpr, Idris.Parser |
| RForce | Core.TT |
| RFunction | Core.TT |
| rhs | Idris.Parser |
| ribbonsPerLine | Util.Pretty |
| RightOK | Idris.AbsSyntax |
| rmFile | Util.System |
| rmIBC | Pkg.Package |
| RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| rparen | Util.Pretty |
| RProgram | Core.TT |
| RType | Core.TT |
| rtype | Core.TT |
| rt_simplify | Core.Evaluate |
| Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| runClient | Idris.REPL |
| runElab | Core.Elaborate |
| runIdris | Main |
| runInnerParser | Idris.ParseHelpers, Idris.Parser |
| runIO | Idris.AbsSyntax |
| runparser | Idris.ParseHelpers, Idris.Parser |
| runTac | Idris.ElabTerm |
| RunTime | Core.CaseTree |
| runtimeExceptionType | IRTS.Java.JTypes |
| RVal | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | IRTS.Bytecode |
| rval | Core.TT |
| SAlt | IRTS.Simplified |
| sAlt | IRTS.Simplified |
| Same | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SApp | IRTS.Simplified |
| saveState | Core.Elaborate |
| SC | Core.CaseTree |
| SC' | Core.CaseTree |
| SCase | IRTS.Simplified |
| scg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SCGEntry | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SChkCase | IRTS.Simplified |
| SCon | IRTS.Simplified |
| SConCase | IRTS.Simplified |
| SConst | IRTS.Simplified |
| SConstCase | IRTS.Simplified |
| scopecheck | IRTS.Simplified |
| score | Core.TT |
| SDecl | IRTS.Simplified |
| SDefaultCase | IRTS.Simplified |
| Search | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| semi | Util.Pretty |
| sep | Util.Pretty |
| serialize | IRTS.DumpBC |
| serializeBC | IRTS.DumpBC |
| serializeCase | IRTS.DumpBC |
| serializeDefault | IRTS.DumpBC |
| serializeReg | IRTS.DumpBC |
| SError | IRTS.Simplified |
| setAccess | Core.Evaluate |
| setAccessibility | Idris.AbsSyntax |
| setAndReport | Idris.Error |
| setCmdLine | Idris.AbsSyntax |
| setCodegen | Idris.AbsSyntax |
| SetColour | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| setColour | Idris.AbsSyntax |
| setColourise | Idris.AbsSyntax |
| setContext | Idris.AbsSyntax |
| setCoverage | Idris.AbsSyntax |
| setErrContext | Idris.AbsSyntax |
| setErrLine | Idris.AbsSyntax |
| setFlags | Idris.AbsSyntax |
| setIBCSubDir | Idris.AbsSyntax |
| setIdeSlave | Idris.AbsSyntax |
| setImportDirs | Idris.AbsSyntax |
| setImpShow | Idris.AbsSyntax |
| setinj | Core.Elaborate |
| SetInjective | Core.ProofState, Core.Elaborate |
| setLogLevel | Idris.AbsSyntax |
| setNoBanner | Idris.AbsSyntax |
| SetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| setOptLevel | Idris.AbsSyntax |
| setOutH | Idris.AbsSyntax |
| setOutputTy | Idris.AbsSyntax |
| setQuiet | Idris.AbsSyntax |
| setREPL | Idris.AbsSyntax |
| setSO | Idris.AbsSyntax |
| setTargetCPU | Idris.AbsSyntax |
| setTargetTriple | Idris.AbsSyntax |
| setTotal | Core.Evaluate |
| setTotality | Idris.AbsSyntax |
| setTypeCase | Idris.AbsSyntax |
| setTypeInType | Idris.AbsSyntax |
| setVerbose | Idris.AbsSyntax |
| set_context | Core.Elaborate |
| SExp | |
| 1 (Type/Class) | Idris.IdeSlave |
| 2 (Type/Class) | IRTS.Simplified |
| SExpable | Idris.IdeSlave |
| SexpList | Idris.IdeSlave |
| sexpToCommand | Idris.IdeSlave |
| SForeign | IRTS.Simplified |
| SFun | IRTS.Simplified |
| shadow | Idris.AbsSyntax |
| shortType | IRTS.Java.JTypes |
| showbasic | Idris.Delaborate |
| showCaseTrees | IRTS.Compiler |
| showCG | Core.TT |
| showCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDeclImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDoc | Idris.Docs |
| showEnv | Core.TT |
| showEnv' | Core.TT |
| showEnvDbg | Core.TT |
| showErr | Idris.Error |
| showImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowImpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowIncs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showIncs | Main |
| ShowLibdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showLibdir | Main |
| ShowLibs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showLibs | Main |
| showName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showProof | Idris.Prover |
| showqual | Idris.Delaborate |
| showSc | Idris.Delaborate |
| showSep | Core.TT |
| showTotal | Idris.REPL |
| showTotalN | Idris.REPL |
| showver | Main |
| sigmaTy | Idris.AbsSyntax |
| simpleCase | Core.CaseTree |
| simpleConstructor | Idris.ParseData, Idris.Parser |
| SimpleExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| simpleExpr | Idris.ParseExpr, Idris.Parser |
| simpleExternalExpr | Idris.ParseExpr, Idris.Parser |
| simpleMethod | IRTS.Java.ASTBuilding |
| simpleWhiteSpace | Idris.ParseHelpers, Idris.Parser |
| simple_app | Core.Elaborate |
| Simplify | Core.ProofState, Core.Elaborate |
| simplify | |
| 1 (Function) | Core.Evaluate |
| 2 (Function) | Core.Elaborate |
| 3 (Function) | IRTS.Simplified |
| simplifyCasedef | Core.Evaluate |
| singleLineComment | Idris.ParseHelpers, Idris.Parser |
| size | Util.Pretty |
| SizeChange | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Sized | Util.Pretty |
| sizedText | Util.Pretty |
| SLet | IRTS.Simplified |
| SLIDE | IRTS.Bytecode |
| small | Core.CaseTree |
| Smaller | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SN | Core.TT |
| sname | |
| 1 (Function) | Idris.Transforms |
| 2 (Function) | IRTS.Compiler |
| SNothing | IRTS.Simplified |
| Solve | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| solve | Core.Elaborate |
| solveAll | Idris.ElabTerm |
| solved | Core.ProofState, Core.Elaborate |
| solveDeferred | Idris.AbsSyntax |
| SOp | IRTS.Simplified |
| sourcedir | Pkg.PParser |
| sourcefile | Idris.IBC |
| sourceTypes | IRTS.Java.JTypes |
| space | Util.Pretty |
| Spec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SpecialHeaderArg | Idris.Help |
| Specialise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| specialise | Core.Evaluate |
| SpecialName | Core.TT |
| specType | Idris.PartialEval |
| splitOnLine | Idris.CaseSplit |
| SProj | IRTS.Simplified |
| srcPath | Idris.Imports |
| SSymbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| startServer | Idris.REPL |
| StartUnify | Core.ProofState, Core.Elaborate |
| start_unify | Core.Elaborate |
| Static | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| static | Idris.ParseExpr, Idris.Parser |
| STerm | Core.CaseTree |
| STOREOLD | IRTS.Bytecode |
| Str | |
| 1 (Data Constructor) | Util.Pretty |
| 2 (Data Constructor) | Core.TT |
| string | Idris.ParseHelpers, Idris.Parser |
| StringAtom | Idris.IdeSlave |
| stringLiteral | Idris.ParseHelpers, Idris.Parser |
| stringType | IRTS.Java.JTypes |
| stripCollapsed | Idris.DataOpts |
| stripLinear | Idris.AbsSyntax |
| stripUnmatchable | Idris.AbsSyntax |
| StrType | Core.TT |
| Style | |
| 1 (Data Constructor) | Util.Pretty |
| 2 (Type/Class) | Util.Pretty |
| style | Util.Pretty |
| subst | Core.TT |
| substMatch | Idris.AbsSyntax |
| substMatches | Idris.AbsSyntax |
| substMatchesShadow | Idris.AbsSyntax |
| substMatchShadow | Idris.AbsSyntax |
| substNames | Core.TT |
| substTerm | Core.TT |
| substV | Core.TT |
| suc | Idris.Transforms |
| SucCase | Core.CaseTree |
| SUpdate | IRTS.Simplified |
| SV | IRTS.Simplified |
| sVar | IRTS.Simplified |
| Symbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| symbol | Idris.ParseHelpers, Idris.Parser |
| SymbolAtom | Idris.IdeSlave |
| Syn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SynBind | Idris.ParseExpr, Idris.Parser |
| SynContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SynMatch | Idris.ParseExpr, Idris.Parser |
| Syntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntaxDecl | Idris.Parser |
| SyntaxInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntaxRule | Idris.Parser |
| syntaxSym | Idris.Parser |
| syntax_keywords | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntax_rules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SynTm | Idris.ParseExpr, Idris.Parser |
| syn_namespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syn_params | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| T | IRTS.Bytecode |
| table | Idris.ParseOps, Idris.Parser |
| Tac | Core.Elaborate |
| TacImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacimpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Tactic | Core.ProofState, Core.Elaborate |
| tactic | Idris.ParseExpr, Idris.Parser |
| tacticsExpr | Idris.ParseExpr, Idris.Parser |
| TAILCALL | IRTS.Bytecode |
| TargetCPU | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| targetCPU | Idris.AbsSyntax |
| TargetTriple | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| targetTriple | Idris.AbsSyntax |
| TC | Core.TT |
| tclift | Idris.Error |
| tcname | Core.TT |
| TCon | Core.TT |
| tctry | Idris.Error |
| tc_dictionary | Core.Evaluate |
| tempfile | Util.System |
| Term | Core.TT |
| terminator | Idris.ParseHelpers, Idris.Parser |
| TermSize | Core.TT |
| termsize | Core.TT |
| TermSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TermTrans | Idris.Transforms |
| TestInline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| testLib | Pkg.Package |
| text | Util.Pretty |
| TextDetails | Util.Pretty |
| tfail | Core.TT |
| Theorem | Core.Elaborate |
| thname | Core.ProofState, Core.Elaborate |
| threadType | IRTS.Java.JTypes |
| TI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| timestampOlder | Idris.IBC |
| tldeclared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Tmp | IRTS.Bytecode |
| toAlist | Core.TT |
| toBC | |
| 1 (Function) | IRTS.BCImp |
| 2 (Function) | IRTS.Bytecode |
| toClassType | IRTS.Java.ASTBuilding |
| toCons | IRTS.Defunctionalise |
| toEither | Idris.AbsSyntax |
| toIBCFile | Pkg.Package |
| ToIR | IRTS.Compiler |
| TOPBASE | IRTS.Bytecode |
| toplevel | Idris.ElabTerm |
| toRefType | IRTS.Java.ASTBuilding |
| toSExp | Idris.IdeSlave |
| toTable | Idris.ParseOps, Idris.Parser |
| Total | Core.Evaluate |
| TotalFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Totality | Core.Evaluate |
| totality | Idris.Parser |
| TotCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| totcheck | Idris.AbsSyntax |
| TRACE | IRTS.CodegenCommon |
| traceUnused | Idris.UnusedArgs |
| traceWhen | Core.TT |
| Transform | Idris.Transforms |
| transform | |
| 1 (Function) | Idris.Transforms |
| 2 (Function) | Idris.Parser |
| Trivial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| trivial | Idris.ProofSearch |
| trivial' | Idris.ElabTerm |
| trun | Core.TT |
| Try | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| try | Core.Elaborate |
| try' | Core.Elaborate |
| tryAll | Core.Elaborate |
| tryLoadLib | Util.DynamicLinker |
| tryWhen | Core.Elaborate |
| TSeq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TT | Core.TT |
| TTOpt | Idris.Transforms |
| TType | Core.TT |
| TTypeInTType | Core.TT |
| tt_ctxt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TyDecl | Core.Evaluate |
| tyOptDeclList | Idris.ParseExpr, Idris.Parser |
| Type | Core.TT |
| TypeCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TypeColour | Idris.Colours |
| typeColour | Idris.Colours |
| typeDeclList | Idris.ParseExpr, Idris.Parser |
| typeExpr | Idris.ParseExpr, Idris.Parser |
| TypeInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TypeInType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| typeInType | Idris.AbsSyntax |
| TypeOf | Idris.IdeSlave |
| TypeProviders | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ucheck | Core.Constraints |
| UConstraint | |
| 1 (Type/Class) | Core.TT |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| uconstraints | Core.Evaluate |
| UCs | Core.TT |
| UExp | Core.TT |
| UImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ULE | Core.TT |
| ULT | Core.TT |
| UN | Core.TT |
| unApply | Core.TT |
| Unchecked | Core.Evaluate |
| underline | Idris.Colours |
| Undo | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| undo | Core.Elaborate |
| unIdiom | Idris.DSL |
| unified | Core.ProofState, Core.Elaborate |
| UnifiedD | Idris.PartialEval |
| unify | Core.Unify |
| unifyLog | |
| 1 (Function) | Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| unifylog | Core.ProofState, Core.Elaborate |
| UnifyProblems | Core.ProofState, Core.Elaborate |
| unifyProblems | Core.Elaborate |
| UnifyScope | Core.TT |
| uniqueBinders | Core.TT |
| uniqueName | Core.TT |
| uniqueNameCtxt | Core.Elaborate |
| unique_hole | Core.Elaborate |
| unique_hole' | Core.Elaborate |
| unitCon | Idris.AbsSyntax |
| unitDecl | Idris.AbsSyntax |
| unitTy | Idris.AbsSyntax |
| UniverseError | Core.TT |
| Universes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Unknown | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unlit | Idris.Unlit |
| UnmatchedCase | Core.CaseTree |
| UnsetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unusedpos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unwrapFC | Core.TT |
| upd | Idris.Coverage |
| UPDATE | IRTS.Bytecode |
| updateAux | Core.Elaborate |
| updateContext | Idris.AbsSyntax |
| updateDef | Core.TT |
| updateN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updateNs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| update_term | Core.Elaborate |
| Usage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usage | Main |
| usagemsg | Main |
| UseCodegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| used | Idris.UnusedArgs |
| usedArg | IRTS.Lang, IRTS.Defunctionalise |
| usedIn | IRTS.Lang, IRTS.Defunctionalise |
| usedNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedns | Core.ProofState, Core.Elaborate |
| useREPL | Idris.AbsSyntax |
| UseUndef | Core.Evaluate |
| Using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usingDecl | Idris.Parser |
| usingDeclList | Idris.Parser |
| using_ | Idris.Parser |
| UVal | Core.TT |
| UVar | Core.TT |
| V | Core.TT |
| valIBCSubDir | Idris.AbsSyntax |
| Value | Core.Evaluate |
| VApp | Core.Evaluate |
| Var | Core.TT |
| var | Idris.DSL |
| VBind | Core.Evaluate |
| VBLet | Core.Evaluate |
| vcat | Util.Pretty |
| VConstant | Core.Evaluate |
| Ver | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ver | |
| 1 (Function) | Idris.IBC |
| 2 (Function) | Idris.REPL |
| VErased | Core.Evaluate |
| Verbose | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| verbose | Idris.AbsSyntax |
| version | Paths_idris |
| ViaC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ViaJava | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ViaJavaScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ViaLLVM | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ViaNode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| VImpossible | Core.Evaluate |
| vinstances | Core.TT |
| vivid | Idris.Colours |
| VoidType | Core.TT |
| voidType | IRTS.Java.JTypes |
| VP | Core.Evaluate |
| VProj | Core.Evaluate |
| VTmp | Core.Evaluate |
| vToP | Core.TT |
| VType | Core.Evaluate |
| VV | Core.Evaluate |
| WarnOnly | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| WarnPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| weakenEnv | Core.TT |
| weakenTm | Core.TT |
| weakenTmEnv | Core.TT |
| wExpr | Idris.Parser |
| whereBlock | Idris.Parser |
| WhereN | Core.TT |
| whiteSpace | Idris.ParseHelpers, Idris.Parser |
| withTempdir | Util.System |
| Wk | Core.TT |
| WkEnv | Core.TT |
| WkEnvTT | Core.TT |
| writeIBC | Idris.IBC |
| zero | Idris.Transforms |
| zeroWidthText | Util.Pretty |
| ZigZagMode | Util.Pretty |
| zname | |
| 1 (Function) | Idris.Transforms |
| 2 (Function) | IRTS.Compiler |
| ~&&~ | IRTS.Java.ASTBuilding |
| ~==~ | IRTS.Java.ASTBuilding |
| ~> | IRTS.Java.ASTBuilding |