Index
| <> | IRTS.Java.ASTBuilding |
| @! | IRTS.Java.ASTBuilding |
| @:= | IRTS.Java.ASTBuilding |
| 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 |
| 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 |
| 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 |
| AnnName | 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 |
| 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 |
| AutoWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| B16 | Idris.Core.TT |
| B16V | Idris.Core.TT |
| B32 | Idris.Core.TT |
| B32V | Idris.Core.TT |
| B64 | Idris.Core.TT |
| B64V | Idris.Core.TT |
| B8 | Idris.Core.TT |
| B8V | Idris.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 |
| bdecode | Idris.IBC |
| BE | IRTS.Lang, IRTS.Defunctionalise |
| BelieveMe | Idris.Core.Evaluate |
| bencode | Idris.IBC |
| BI | Idris.Core.TT |
| bi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Bigger | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bigInteger | IRTS.Java.ASTBuilding |
| bigIntegerType | IRTS.Java.JTypes |
| binary | Idris.ParseOps, Idris.Parser |
| Bind | Idris.Core.TT |
| bindAll | Idris.Core.TT |
| Binder | Idris.Core.TT |
| binderTy | Idris.Core.TT |
| binderVal | Idris.Core.TT |
| Binding | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bindingOf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bindList | Idris.ParseHelpers, Idris.Parser |
| bindTyArgs | Idris.Core.TT |
| bold | Idris.Colours |
| BoolAtom | Idris.IdeSlave |
| Bound | Idris.Core.TT |
| boundNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| BoundVarColour | Idris.Colours |
| boundVarColour | Idris.Colours |
| box | IRTS.Java.JTypes |
| brace_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bracketed | Idris.ParseExpr, Idris.Parser |
| bracketedExpr | Idris.ParseExpr, Idris.Parser |
| BufferType | Idris.Core.TT |
| 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 |
| ByReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 | Idris.Core.TT |
| CantInferType | Idris.Core.TT |
| CantIntroduce | Idris.Core.TT |
| CantResolve | Idris.Core.TT |
| CantResolveAlts | Idris.Core.TT |
| CantSolveGoal | Idris.Core.TT |
| CantUnify | Idris.Core.TT |
| CASE | IRTS.Bytecode |
| Case | Idris.Core.CaseTree |
| CaseAlt | Idris.Core.CaseTree |
| caseAlt | IRTS.Bytecode |
| CaseAlt' | Idris.Core.CaseTree |
| CaseDef | |
| 1 (Type/Class) | Idris.Core.CaseTree |
| 2 (Data Constructor) | Idris.Core.CaseTree |
| CaseDefs | |
| 1 (Type/Class) | Idris.Core.Evaluate |
| 2 (Data Constructor) | Idris.Core.Evaluate |
| caseExpr | Idris.ParseExpr, Idris.Parser |
| CaseInfo | |
| 1 (Type/Class) | Idris.Core.Evaluate |
| 2 (Data Constructor) | Idris.Core.Evaluate |
| CaseN | Idris.Core.TT |
| CaseOp | Idris.Core.Evaluate |
| caseOption | Idris.ParseExpr, Idris.Parser |
| CaseSplit | Idris.IdeSlave |
| CaseSplitAt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| cases_compiletime | Idris.Core.Evaluate |
| cases_inlined | Idris.Core.Evaluate |
| cases_runtime | Idris.Core.Evaluate |
| cases_totcheck | Idris.Core.Evaluate |
| CaseTrans | Idris.Transforms |
| CaseTree | Idris.Core.CaseTree |
| case_inlinable | Idris.Core.Evaluate |
| CExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CGInfo | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ch | Idris.Core.TT |
| ChangeDirectory | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| char | Idris.ParseHelpers, Idris.Parser |
| charLiteral | Idris.ParseHelpers, Idris.Parser |
| charType | IRTS.Java.JTypes |
| Check | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| check | Idris.Core.Typecheck |
| check' | Idris.Core.Typecheck |
| CheckConv | Idris.Core.TT |
| checkDeclTotality | Idris.Coverage |
| checkDef | Idris.ElabDecls |
| checkDefs | IRTS.Simplified |
| checkDSL | Idris.ParseData, Idris.Parser |
| CheckIn | Idris.Core.ProofState, Idris.Core.Elaborate |
| checkInferred | Idris.ElabDecls |
| checkInjective | Idris.Core.Elaborate |
| checkMP | Idris.Coverage |
| checkPiGoal | Idris.Core.Elaborate |
| checkPkg | Pkg.Package |
| checkPositive | Idris.Coverage |
| checkPossible | Idris.ElabDecls |
| checkSizeChange | Idris.Coverage |
| checkTotality | Idris.Coverage |
| checkUndefined | Idris.AbsSyntax |
| check_in | Idris.Core.Elaborate |
| CI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Claim | Idris.Core.ProofState, Idris.Core.Elaborate |
| claim | Idris.Core.Elaborate |
| classBlock | Idris.Parser |
| ClassDoc | Idris.Docs |
| ClassInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| classInfo | Idris.REPL |
| class_ | Idris.Parser |
| class_defaults | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_default_superclasses | 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 |
| clearOrigPats | Idris.AbsSyntax |
| clearPTypes | 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 |
| codata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegen | Idris.AbsSyntax |
| codegenC | IRTS.CodegenC |
| codegenJava | IRTS.CodegenJava |
| codegenJavaScript | IRTS.CodegenJavaScript |
| 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 |
| 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 |
| ColsWide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| columnNum | Idris.ParseHelpers, Idris.Parser |
| Command | |
| 1 (Type/Class) | Idris.Core.Elaborate |
| 2 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Compile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compile | IRTS.Compiler |
| compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CompileTime | Idris.Core.CaseTree |
| CompleteFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| complete_fill | Idris.Core.Elaborate |
| comprehension | Idris.ParseExpr, Idris.Parser |
| Compute | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compute | Idris.Core.Elaborate |
| ComputeLet | Idris.Core.ProofState, Idris.Core.Elaborate |
| computeLet | Idris.Core.Elaborate |
| ConCase | Idris.Core.CaseTree |
| conCase | IRTS.Bytecode |
| Conditional | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| consoleDecorate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| consoleDisplayAnnotated | Idris.AbsSyntax |
| ConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ConsoleWidthArg | Idris.Help |
| Const | Idris.Core.TT |
| constAlt | IRTS.Bytecode |
| Constant | Idris.Core.TT |
| constant | Idris.ParseExpr, Idris.Parser |
| CONSTCASE | IRTS.Bytecode |
| ConstCase | Idris.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 | Idris.Core.Evaluate |
| context | Idris.Core.ProofState, Idris.Core.Elaborate |
| contextArray | IRTS.Java.JTypes |
| contextParam | IRTS.Java.JTypes |
| convEq | Idris.Core.Evaluate |
| convEq' | Idris.Core.Evaluate |
| converts | Idris.Core.Typecheck |
| convertsC | Idris.Core.Typecheck |
| convSExp | Idris.IdeSlave |
| con_names | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| coverage | Idris.AbsSyntax |
| Ctxt | Idris.Core.TT |
| ctxtAlist | Idris.Core.Evaluate |
| DAlt | IRTS.Defunctionalise |
| DApp | IRTS.Defunctionalise |
| Data | Idris.Core.TT |
| DataColour | Idris.Colours |
| dataColour | Idris.Colours |
| DataDoc | Idris.Docs |
| DataErrRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dataI | Idris.ParseData, Idris.Parser |
| DataMI | Idris.Core.Evaluate |
| DataOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DataOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dataOpts | Idris.ParseData, Idris.Parser |
| DataOutput | Idris.Core.TT |
| Datatype | Idris.Core.TT |
| data_ | Idris.ParseData, Idris.Parser |
| data_opts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DbgLevel | IRTS.CodegenCommon |
| DC | IRTS.Defunctionalise |
| DCase | IRTS.Defunctionalise |
| DChkCase | IRTS.Defunctionalise |
| DCon | Idris.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 | Idris.Core.Evaluate |
| defaultAlt | IRTS.Bytecode |
| DefaultCase | Idris.Core.CaseTree |
| DefaultEliminator | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DefaultPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 | Idris.Core.ProofState, Idris.Core.Elaborate |
| defer | Idris.Core.Elaborate |
| deferred | Idris.Core.ProofState, Idris.Core.Elaborate |
| DeferType | Idris.Core.ProofState, Idris.Core.Elaborate |
| deferType | Idris.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 |
| delabMV | 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 |
| disamb | Idris.ParseExpr, Idris.Parser |
| discard | Idris.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) | Idris.Docs |
| 2 (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 | Idris.Core.ProofState, Idris.Core.Elaborate |
| dontunify | Idris.Core.ProofState, Idris.Core.Elaborate |
| DOp | IRTS.Defunctionalise |
| DoProofSearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| doubleType | IRTS.Java.JTypes |
| do_ | Idris.ParseExpr, Idris.Parser |
| DProj | IRTS.Defunctionalise |
| dropGiven | Idris.Core.ProofState, Idris.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 |
| dumpDefaultInstance | Idris.REPL |
| DumpDefun | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dumpDefuns | IRTS.Defunctionalise |
| dumpInstance | Idris.REPL |
| dumpMethod | Idris.REPL |
| dumpprobs | Idris.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) | Idris.Core.TT |
| 2 (Function) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_tcon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| d_type | Idris.Core.TT |
| d_typename | Idris.Core.TT |
| d_typetag | Idris.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 | Idris.Core.Elaborate |
| elab | Idris.ElabTerm |
| Elab' | Idris.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 |
| elabEliminator | Idris.ElabDecls |
| ElabInfo | Idris.ElabTerm |
| elabInstance | Idris.ElabDecls |
| elaborate | Idris.Core.Elaborate |
| Elaborating | Idris.Core.TT |
| elabPE | Idris.ElabDecls |
| elabPostulate | Idris.ElabDecls |
| elabPrims | Idris.ElabDecls |
| elabProvider | Idris.ElabDecls |
| elabRecord | Idris.ElabDecls |
| ElabState | Idris.Core.Elaborate |
| elabStep | Idris.Prover |
| elabTransform | Idris.ElabDecls |
| elabType | Idris.ElabDecls |
| elabType' | Idris.ElabDecls |
| elabVal | Idris.ElabDecls |
| elabValBind | Idris.ElabDecls |
| ElabWhat | Idris.ElabDecls |
| elimDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EliminatorState | Idris.ElabDecls |
| elimMethElim | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elimMethElimTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ElimN | Idris.Core.TT |
| elimName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elog | Idris.Core.Elaborate |
| emptyContext | Idris.Core.TT |
| emptyFC | Idris.Core.TT |
| EmptyMI | Idris.Core.Evaluate |
| Endianness | IRTS.Lang, IRTS.Defunctionalise |
| EndUnify | Idris.Core.ProofState, Idris.Core.Elaborate |
| end_unify | Idris.Core.Elaborate |
| Env | Idris.Core.TT |
| envAtFocus | Idris.Core.ProofState, Idris.Core.Elaborate |
| environment | IRTS.CodegenCommon |
| envlen | Idris.Core.TT |
| EnvTT | Idris.Core.TT |
| envTupleType | Idris.ElabTerm |
| eol | Idris.ParseHelpers, Idris.Parser |
| eqCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqProp | Idris.ParseHelpers, Idris.Parser |
| eqTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Equiv | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| equiv | Idris.Core.Elaborate |
| Erased | Idris.Core.TT |
| Err | Idris.Core.TT |
| Err' | Idris.Core.TT |
| errAt | Idris.Core.Elaborate |
| ErrContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| errContext | Idris.AbsSyntax |
| errEnv | Idris.Core.Typecheck |
| errLine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ERROR | IRTS.Bytecode |
| Error | Idris.Core.TC, Idris.Core.TT |
| ErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ErrorReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ErrorReportPart | Idris.Core.TT |
| ErrorReverse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| errReverse | Idris.ErrReverse |
| erun | Idris.Core.Elaborate |
| ES | Idris.Core.Elaborate |
| ETypes | Idris.ElabDecls |
| Eval | |
| 1 (Data Constructor) | Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EvalApply | IRTS.Defunctionalise |
| EvalCase | IRTS.Defunctionalise |
| evalD | IRTS.Inliner |
| EvalIn | Idris.Core.ProofState, Idris.Core.Elaborate |
| eval_in | Idris.Core.Elaborate |
| Exact | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| exact | Idris.Core.Elaborate |
| exceptionType | IRTS.Java.JTypes |
| execElab | Idris.Core.Elaborate |
| execScript | Idris.REPL |
| Executable | IRTS.CodegenCommon |
| Execute | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| execute | Idris.Core.Execute |
| ExecVal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| existsCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Exp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expandDo | Idris.DSL |
| ExpandLet | Idris.Core.ProofState, Idris.Core.Elaborate |
| expandLet | Idris.Core.Elaborate |
| expandNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expandParams | Idris.AbsSyntax |
| expandParamsD | Idris.AbsSyntax |
| expl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| explicit | Idris.Core.Elaborate |
| ExplicitD | Idris.PartialEval |
| explicitNames | Idris.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 |
| failMsg | Idris.Core.TT |
| Fails | Idris.Core.Unify |
| falseDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| falseOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| falseTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fancifyAnnots | Idris.AbsSyntax |
| FAny | IRTS.Lang, IRTS.Defunctionalise |
| FArith | IRTS.Lang, IRTS.Defunctionalise |
| FC | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.Core.TT |
| FC' | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.Core.TT |
| FCallType | IRTS.Lang, IRTS.Defunctionalise |
| FConstructor | IRTS.Lang, IRTS.Defunctionalise |
| fc_column | Idris.Core.TT |
| fc_fname | Idris.Core.TT |
| fc_line | Idris.Core.TT |
| FFunction | IRTS.Lang, IRTS.Defunctionalise |
| FFunctionIO | IRTS.Lang, IRTS.Defunctionalise |
| FileArg | Idris.Help |
| fileFC | Idris.Core.TT |
| Filename | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fileName | Idris.ParseHelpers, Idris.Parser |
| Fill | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fill | Idris.Core.Elaborate |
| finalise | Idris.Core.TT |
| findCalls | Idris.Core.CaseTree |
| findFC | Idris.Parser |
| findImport | Idris.Imports |
| findInPath | Idris.Imports |
| findInstances | Idris.ElabTerm |
| findStatics | Idris.AbsSyntax |
| findUnusedArgs | Idris.UnusedArgs |
| findUsedArgs | Idris.Core.CaseTree |
| 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 | Idris.Core.TT |
| FLang | IRTS.Lang, IRTS.Defunctionalise |
| float | Idris.ParseHelpers, Idris.Parser |
| fmapMB | Idris.Core.TT |
| FnCase | Idris.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) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| focus | Idris.Core.Elaborate |
| Forall | Idris.Core.ProofState, Idris.Core.Elaborate |
| forall | Idris.Core.Elaborate |
| Forceability | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| forceable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| forceArgs | Idris.DataOpts |
| forcedArgSeq | Idris.DataOpts |
| forcedCnt | Idris.DataOpts |
| ForceMap | Idris.DataOpts |
| force_term | Idris.Core.Elaborate |
| forCodegen | Idris.AbsSyntax |
| FOREIGNCALL | IRTS.Bytecode |
| foreignType | IRTS.Java.JTypes |
| foreignWrapperType | IRTS.Java.JTypes |
| forget | Idris.Core.TT |
| Forgot | Idris.Core.TT |
| FPtr | IRTS.Lang, IRTS.Defunctionalise |
| freeNames | Idris.Core.TT |
| fromTTMaybe | Idris.ElabTerm |
| Frozen | Idris.Core.Evaluate |
| FStatic | IRTS.Lang, IRTS.Defunctionalise |
| FString | IRTS.Lang, IRTS.Defunctionalise |
| FType | IRTS.Lang, IRTS.Defunctionalise |
| fullExpr | Idris.ParseExpr, Idris.Parser |
| fullTactic | Idris.ParseExpr, Idris.Parser |
| Function | Idris.Core.Evaluate |
| FunctionColour | Idris.Colours |
| functionColour | Idris.Colours |
| FunDoc | |
| 1 (Data Constructor) | Idris.Docs |
| 2 (Type/Class) | Idris.Docs |
| FUnit | IRTS.Lang, IRTS.Defunctionalise |
| FunOutput | Idris.Core.TT |
| GD | Idris.Core.ProofState, Idris.Core.Elaborate |
| genAll | Idris.Coverage |
| genArgs | IRTS.Defunctionalise |
| genClauses | Idris.Coverage |
| getAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getAllNames | Idris.AbsSyntax |
| getArgTys | Idris.Core.TT |
| getAux | Idris.Core.Elaborate |
| getBC | Idris.REPL |
| getCC | IRTS.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 |
| getDocs | Idris.Docs |
| getDumpCases | Idris.AbsSyntax |
| getDumpDefun | Idris.AbsSyntax |
| getErrColumn | Idris.Error |
| getErrLine | Idris.Error |
| getExecScript | Idris.REPL |
| getExecutablePom | IRTS.System |
| getExps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getFargpos | Idris.UnusedArgs |
| getFC | Idris.ParseHelpers, Idris.Parser |
| getFile | Idris.REPL |
| getFlags | Idris.AbsSyntax |
| getFn | IRTS.Defunctionalise |
| getForcedArgs | Idris.DataOpts |
| getFTypes | IRTS.Compiler |
| getFunctionErrorHandlers | Idris.AbsSyntax |
| getHdrs | Idris.AbsSyntax |
| getIBCSubDir | Idris.REPL |
| getIdrisLibDir | IRTS.System |
| getIdrisUserDataDir | Idris.REPL |
| getImportDir | Idris.REPL |
| getImps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getIncFlags | IRTS.System |
| getInferTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getInferType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getInitScript | Idris.REPL |
| getInternalApp | Idris.AbsSyntax |
| getIState | Idris.AbsSyntax |
| getLanguageExt | Idris.REPL |
| getLibFlags | IRTS.System |
| getLibs | Idris.AbsSyntax |
| getLog | Idris.Core.Elaborate |
| getModuleFiles | Idris.Chaser |
| getMvn | IRTS.System |
| getName | Idris.AbsSyntax |
| getNameFrom | Idris.Core.Elaborate |
| getNameHints | 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 |
| getPkgCheck | Idris.REPL |
| getPkgClean | Idris.REPL |
| getPkgDir | Idris.REPL |
| getPkgREPL | Idris.REPL |
| getPrim | IRTS.Compiler |
| getPriority | Idris.AbsSyntax |
| getProofClause | Idris.CaseSplit |
| getProvided | Idris.Providers |
| getQuiet | Idris.AbsSyntax |
| getRetTy | Idris.Core.TT |
| getScreenWidth | Util.ScreenSize |
| getScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getSO | Idris.AbsSyntax |
| getSpecApps | Idris.PartialEval |
| getTargetDir | IRTS.System |
| getTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getTotality | Idris.AbsSyntax |
| getTriple | Idris.REPL |
| getUndefined | Idris.AbsSyntax |
| getUnifyLog | Idris.Core.Elaborate |
| getUniq | Idris.CaseSplit |
| getWidth | Idris.AbsSyntax |
| get_context | Idris.Core.Elaborate |
| get_deferred | Idris.Core.Elaborate |
| get_env | Idris.Core.Elaborate |
| get_guess | Idris.Core.Elaborate |
| get_holes | Idris.Core.Elaborate |
| get_instances | Idris.Core.Elaborate |
| get_probs | Idris.Core.Elaborate |
| get_term | Idris.Core.Elaborate |
| get_type | Idris.Core.Elaborate |
| get_type_val | Idris.Core.Elaborate |
| GHole | Idris.Core.TT |
| Glob | IRTS.Lang, IRTS.Defunctionalise |
| globalContext | IRTS.Java.JTypes |
| globalContextID | IRTS.Java.JTypes |
| Goal | Idris.Core.ProofState, Idris.Core.Elaborate |
| goal | Idris.Core.Elaborate |
| goalAtFocus | Idris.Core.ProofState, Idris.Core.Elaborate |
| GoalType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| goalType | Idris.Core.ProofState, Idris.Core.Elaborate |
| groupsOf | IRTS.Defunctionalise |
| gteProp | Idris.ParseHelpers, Idris.Parser |
| gtProp | Idris.ParseHelpers, Idris.Parser |
| Guess | Idris.Core.TT |
| Help | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| help | Idris.Help |
| helphead | Idris.REPL |
| Hidden | Idris.Core.Evaluate |
| HideDisplay | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| hide_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| HNF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| hnf | Idris.Core.Evaluate |
| HNF_Compute | Idris.Core.ProofState, Idris.Core.Elaborate |
| hnf_compute | Idris.Core.Elaborate |
| Hole | Idris.Core.TT |
| holes | Idris.Core.ProofState, Idris.Core.Elaborate |
| hsimpleExpr | Idris.ParseExpr, Idris.Parser |
| hvar | IRTS.Simplified |
| I | Idris.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 |
| IBCErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCErrRev | 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 |
| IBCFunctionErrorHandler | 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 |
| IBCMetaInformation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCNameHint | 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_errorhandlers | Idris.IBC |
| ibc_errRev | Idris.IBC |
| ibc_fixes | Idris.IBC |
| ibc_flags | Idris.IBC |
| ibc_function_errorhandlers | 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_metainformation | Idris.IBC |
| ibc_namehints | 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 |
| ideSlaveReturnAnnotated | 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_consolewidth | 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_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_errRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_flags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_function_errorhandlers | 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_metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_namehints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_nameIdx | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_objs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_optimisation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_options | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| ihPrintFunTypes | Idris.AbsSyntax |
| ihPrintResult | Idris.AbsSyntax |
| ihPrintTermWithType | Idris.AbsSyntax |
| ihputStrLn | Idris.AbsSyntax |
| ihRenderResult | 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 | Idris.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 | Idris.Core.TT |
| ImpossibleCase | Idris.Core.CaseTree |
| impShow | Idris.AbsSyntax |
| Inaccessible | Idris.Core.TT |
| iName | Idris.ParseHelpers, Idris.Parser |
| inblock | Idris.ElabTerm |
| IncompleteTerm | Idris.Core.TT |
| indent | |
| 1 (Function) | IRTS.DumpBC |
| 2 (Function) | Idris.ParseHelpers, Idris.Parser |
| indented | 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 |
| Induction | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| induction | Idris.Core.Elaborate |
| inferCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inferredDiff | Idris.ElabDecls |
| inferTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InfinitelyWide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InfiniteUnify | Idris.Core.TT |
| Infixl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InfixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Infixr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Info | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initContext | Idris.Core.Evaluate |
| initDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initElaborator | Idris.Core.Elaborate |
| initEval | Idris.Core.Evaluate |
| initIBC | Idris.IBC |
| initNextNameFrom | Idris.Core.Elaborate |
| initScript | Idris.REPL |
| initsEndAt | Idris.ParseHelpers, Idris.Parser |
| injective | Idris.Core.ProofState, Idris.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 | Idris.Core.ProofState, Idris.Core.Elaborate |
| instanceArg | Idris.Core.Elaborate |
| instanceBlock | Idris.Parser |
| InstanceN | Idris.Core.TT |
| instanceName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| instances | Idris.Core.ProofState, Idris.Core.Elaborate |
| instance_ | Idris.Parser |
| instantiate | Idris.Core.TT |
| integer | Idris.ParseHelpers, Idris.Parser |
| IntegerAtom | Idris.IdeSlave |
| integerType | IRTS.Java.JTypes |
| interMap | IRTS.DumpBC |
| internalExpr | Idris.ParseExpr, Idris.Parser |
| InternalMsg | Idris.Core.TT |
| Interpret | Idris.IdeSlave |
| InterpretScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Intro | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| intro | Idris.Core.Elaborate |
| Intros | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IntroTy | Idris.Core.ProofState, Idris.Core.Elaborate |
| introTy | Idris.Core.Elaborate |
| IntTy | Idris.Core.TT |
| intTyName | Idris.Core.TT |
| intTyToJType | IRTS.Java.JTypes |
| intTyWidth | Idris.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 |
| iRender | Idris.AbsSyntax |
| irMain | IRTS.Compiler |
| isArray | IRTS.Java.JTypes |
| isCon | IRTS.Compiler |
| isConName | Idris.Core.Evaluate |
| isConst | IRTS.Bytecode |
| isDConName | Idris.Core.Evaluate |
| isDocCommentMarker | Idris.ParseHelpers, Idris.Parser |
| isEol | Idris.ParseHelpers, Idris.Parser |
| isetPrompt | Idris.AbsSyntax |
| isFloating | IRTS.Java.JTypes |
| isFnName | Idris.Core.Evaluate |
| isInjective | Idris.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 | Idris.Core.Evaluate |
| IsTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IsType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isType | Idris.Core.Typecheck |
| isUndefined | Idris.AbsSyntax |
| IT16 | Idris.Core.TT |
| IT32 | Idris.Core.TT |
| IT64 | Idris.Core.TT |
| IT8 | Idris.Core.TT |
| italic | Idris.Colours |
| ITBig | Idris.Core.TT |
| itBitsName | Idris.Core.TT |
| ITChar | Idris.Core.TT |
| ITFixed | Idris.Core.TT |
| ITNative | Idris.Core.TT |
| Itself | Idris.Core.Evaluate |
| ITVec | Idris.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 | Idris.Core.ProofState, Idris.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 |
| LAllocate | IRTS.Lang, IRTS.Defunctionalise |
| LAlt | IRTS.Lang, IRTS.Defunctionalise |
| Lam | Idris.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 |
| LAppend | IRTS.Lang, IRTS.Defunctionalise |
| LAppendBuffer | IRTS.Lang, IRTS.Defunctionalise |
| LASHR | IRTS.Lang, IRTS.Defunctionalise |
| lastIndent | Idris.ParseHelpers, Idris.Parser |
| lastParse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Lazy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| lazyarg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LBitCast | IRTS.Lang, IRTS.Defunctionalise |
| 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 |
| LE | IRTS.Lang, IRTS.Defunctionalise |
| LeftErr | Idris.AbsSyntax |
| LEq | IRTS.Lang, IRTS.Defunctionalise |
| LError | IRTS.Lang, IRTS.Defunctionalise |
| Let | Idris.Core.TT |
| LetBind | Idris.Core.ProofState, Idris.Core.Elaborate |
| letbind | Idris.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 |
| 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 |
| 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 |
| ListErrorHandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 | Idris.Core.TT |
| loadInputs | Idris.REPL |
| loadModule | Idris.Parser |
| loadModule' | Idris.Parser |
| loadSource | Idris.Parser |
| loadSource' | Idris.Parser |
| loadState | Idris.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 | Idris.Core.TT |
| lookupCtxtExact | Idris.Core.TT |
| lookupCtxtName | Idris.Core.TT |
| lookupDef | Idris.Core.Evaluate |
| lookupDefAcc | Idris.Core.Evaluate |
| lookupMetaInformation | Idris.Core.Evaluate |
| lookupNames | Idris.Core.Evaluate |
| lookupNameTotal | Idris.Core.Evaluate |
| lookupP | Idris.Core.Evaluate |
| lookupTotal | Idris.Core.Evaluate |
| lookupTy | Idris.Core.Evaluate |
| lookupTyEnv | Idris.Core.Evaluate |
| lookupVal | Idris.Core.Evaluate |
| LOp | IRTS.Lang, IRTS.Defunctionalise |
| LOpt | IRTS.Lang, IRTS.Defunctionalise |
| LOr | IRTS.Lang, IRTS.Defunctionalise |
| LPar | IRTS.Lang, IRTS.Defunctionalise |
| LPeek | IRTS.Lang, IRTS.Defunctionalise |
| 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 |
| make | Pkg.Package |
| MakeWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MakeWithBlock | Idris.IdeSlave |
| mangle | IRTS.Java.Mangling |
| mangle' | IRTS.Java.Mangling |
| mangleFull | IRTS.Java.Mangling |
| mangleWithPrefix | IRTS.Java.Mangling |
| mapCtxt | Idris.Core.TT |
| mapDefCtxt | Idris.Core.Evaluate |
| mapPT | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapsnd | Idris.AbsSyntax |
| MArgTy | Idris.ElabDecls |
| matchApp | Idris.ParseExpr, Idris.Parser |
| matchClause | Idris.AbsSyntax |
| matchClause' | Idris.AbsSyntax |
| MatchFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| MatchProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
| matchProblems | Idris.Core.Elaborate |
| MatchRefine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| match_apply | Idris.Core.Elaborate |
| match_fill | Idris.Core.Elaborate |
| match_unify | Idris.Core.Unify |
| mathType | IRTS.Java.JTypes |
| MavenProject | IRTS.CodegenCommon |
| maybeWithNS | Idris.ParseHelpers, Idris.Parser |
| MetaInformation | Idris.Core.Evaluate |
| MetaVarArg | Idris.Help |
| Metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MethodN | Idris.Core.TT |
| Missing | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mkApp | Idris.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 |
| mkType | Idris.ParseExpr, Idris.Parser |
| mkUnderCon | IRTS.Defunctionalise |
| mkUniqueNames | Idris.AbsSyntax |
| mkWith | Idris.CaseSplit |
| MN | Idris.Core.TT |
| modifyConst | Idris.ParseExpr, Idris.Parser |
| ModImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ModuleArg | Idris.Help |
| moduleHeader | Idris.Parser |
| ModuleTree | Idris.Chaser |
| module_aliases | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mod_deps | Idris.Chaser |
| mod_needsRecheck | Idris.Chaser |
| mod_path | Idris.Chaser |
| mod_time | Idris.Chaser |
| MonadicParsing | Idris.ParseHelpers, Idris.Parser |
| MoveLast | Idris.Core.ProofState, Idris.Core.Elaborate |
| movelast | Idris.Core.Elaborate |
| moveReg | IRTS.Bytecode |
| Msg | Idris.Core.TT |
| MTree | Idris.Chaser |
| multiLineComment | Idris.ParseHelpers, Idris.Parser |
| MultiPath | Idris.Coverage |
| Mutual | Idris.Core.Evaluate |
| mutual | Idris.Parser |
| Name | Idris.Core.TT |
| name | Idris.ParseHelpers, Idris.Parser |
| NameArg | Idris.Help |
| nameMissing | Idris.CaseSplit |
| NameOutput | Idris.Core.TT |
| NamePart | Idris.Core.TT |
| nameRoot | Idris.CaseSplit |
| namesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| namespace | |
| 1 (Function) | Idris.ElabTerm |
| 2 (Function) | Idris.Parser |
| namesUsed | Idris.Core.CaseTree |
| NameType | Idris.Core.TT |
| natcase | Idris.Transforms |
| Native | IRTS.Lang, IRTS.Defunctionalise |
| NativeTy | Idris.Core.TT |
| nativeTyToJType | IRTS.Java.JTypes |
| nativeTyWidth | Idris.Core.TT |
| natTrans | Idris.Transforms |
| natural | Idris.ParseHelpers, Idris.Parser |
| NErased | Idris.Core.TT |
| newContext | IRTS.Java.JTypes |
| newContextID | IRTS.Java.JTypes |
| newProof | Idris.Core.ProofState, Idris.Core.Elaborate |
| nextName | Idris.Core.TT |
| nextname | Idris.Core.ProofState, Idris.Core.Elaborate |
| next_tvar | Idris.Core.Evaluate |
| NLet | Idris.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 | Idris.Core.TT |
| NONE | IRTS.CodegenCommon |
| NonFunctionType | Idris.Core.TT |
| noOccurrence | Idris.Core.TT |
| NOP | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| noPartial | Idris.Coverage |
| NoPrelude | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoRewriting | Idris.Core.TT |
| normalise | Idris.Core.Evaluate |
| normaliseAll | Idris.Core.Evaluate |
| normaliseC | Idris.Core.Evaluate |
| normaliseTrace | Idris.Core.Evaluate |
| NoSuchVariable | Idris.Core.TT |
| NotCovering | Idris.Core.Evaluate |
| notEndApp | Idris.ParseHelpers, Idris.Parser |
| notEndBlock | Idris.ParseHelpers, Idris.Parser |
| NotEquality | Idris.Core.TT |
| NotInjective | Idris.Core.TT |
| notOpenBraces | Idris.ParseHelpers, Idris.Parser |
| NotPositive | Idris.Core.Evaluate |
| NotProductive | Idris.Core.Evaluate |
| notunified | Idris.Core.ProofState, Idris.Core.Elaborate |
| NoTypeDecl | Idris.Core.TT |
| no_errors | Idris.Core.Elaborate |
| no_imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NS | Idris.Core.TT |
| nsroot | Idris.Core.TT |
| nt_arity | Idris.Core.TT |
| nt_tag | Idris.Core.TT |
| NULL | IRTS.Bytecode |
| Object | IRTS.CodegenCommon |
| objectType | IRTS.Java.JTypes |
| OK | Idris.Core.TC, Idris.Core.TT |
| OLogging | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OP | IRTS.Bytecode |
| opChars | Idris.ParseHelpers, Idris.Parser |
| openBlock | Idris.ParseHelpers, Idris.Parser |
| Operator | Idris.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 | Idris.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_origerr | 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 | Idris.Core.TT |
| Other | Idris.Core.Evaluate |
| Output | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OutputAnnotation | Idris.Core.TT |
| OutputMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OutputTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| outputTy | Idris.AbsSyntax |
| OutputType | IRTS.CodegenCommon |
| overload | Idris.ParseData, Idris.Parser |
| P | Idris.Core.TT |
| pAccess | Idris.IBC |
| pairCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pairDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pairOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pairTy | Idris.AbsSyntaxTree, 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 |
| ParentN | Idris.Core.TT |
| PArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PArg' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pargdoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pargopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parseArgs | Idris.REPL |
| parseCmd | Idris.REPLParser |
| parseCodegen | Idris.REPL |
| parseExpr | Idris.Parser |
| parseImports | Idris.Parser |
| parseMessage | Idris.IdeSlave |
| parseProg | Idris.Parser |
| parseTactic | Idris.Parser |
| Partial | Idris.Core.Evaluate |
| PartialFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| partial_eval | Idris.PartialEval |
| PatBind | Idris.Core.ProofState, Idris.Core.Elaborate |
| patbind | Idris.Core.Elaborate |
| Pattelab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pattern | Idris.Parser |
| PatternSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PatVar | Idris.Core.ProofState, Idris.Core.Elaborate |
| patvar | Idris.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' | 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 |
| PDisamb | 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 |
| pEraseType | Idris.Core.TT |
| pErrorHandlers | Idris.IBC |
| pErrRev | Idris.IBC |
| 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 |
| pFunctionErrorHandlers | Idris.IBC |
| PGoal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Phase | Idris.Core.CaseTree |
| pHdrs | Idris.IBC |
| PHidden | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Pi | Idris.Core.TT |
| pi | Idris.ParseExpr, Idris.Parser |
| piBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| piBindp | Idris.AbsSyntaxTree, 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 |
| PkgCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgClean | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgInstall | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 | Idris.Core.ProofState, Idris.Core.Elaborate |
| ploop | Idris.Prover |
| pmap | Idris.Core.TT |
| PMatchApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pMetaInformation | Idris.IBC |
| PMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMutual | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pNameHints | Idris.IBC |
| 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 |
| PPatvar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pprintErr | Idris.Delaborate |
| pprintPTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProvider | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PReason | Idris.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 |
| prel | Idris.DataOpts |
| premises | Idris.Core.ProofState, Idris.Core.Elaborate |
| prepare_apply | Idris.Core.Elaborate |
| PrepFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| prep_fill | Idris.Core.Elaborate |
| PResolveTC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prettyEnv | Idris.Core.TT |
| prettyImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prettyName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PReturn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| previous | Idris.Core.ProofState, Idris.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.AbsSyntaxTree, Idris.AbsSyntax |
| Idris.Core.Elaborate | |
| priority | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| problems | Idris.Core.ProofState, Idris.Core.Elaborate |
| process | |
| 1 (Function) | Idris.IBC |
| 2 (Function) | Idris.REPL |
| processInput | Idris.REPL |
| processNetCmd | Idris.REPL |
| processTactic | Idris.Core.ProofState, Idris.Core.Elaborate |
| processTactic' | Idris.Core.Elaborate |
| Productive | Idris.Core.Evaluate |
| prog | Idris.Parser |
| ProgramLineComment | Idris.Core.TT |
| Proj | Idris.Core.TT |
| ProjCase | Idris.Core.CaseTree |
| PROJECT | IRTS.Bytecode |
| PROJECTINTO | IRTS.Bytecode |
| PromptColour | Idris.Colours |
| promptColour | Idris.Colours |
| proof | Idris.Core.Elaborate |
| proofExpr | Idris.ParseExpr, Idris.Parser |
| proofFail | Idris.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 | Idris.Core.TT |
| ProofState | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Type/Class) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 3 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofstate | Idris.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 | Idris.Core.TT |
| providerTy | Idris.Providers |
| pruneAlt | Idris.ElabTerm |
| pruneByType | Idris.ElabTerm |
| prunStateT | Idris.Core.Elaborate |
| PS | Idris.Core.ProofState, Idris.Core.Elaborate |
| pscript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pshow | Idris.Delaborate |
| psolve | Idris.ElabDecls |
| pstatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pStatics | Idris.IBC |
| psubst | Idris.Core.TT |
| 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 | Idris.Core.ProofState, Idris.Core.Elaborate |
| pTotal | Idris.IBC |
| pToV | Idris.Core.TT |
| pToV' | Idris.Core.TT |
| pToVs | Idris.Core.TT |
| pTrans | Idris.IBC |
| PTransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PtrType | Idris.Core.TT |
| PTrue | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ptype | Idris.Core.ProofState, Idris.Core.Elaborate |
| PTyped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Public | Idris.Core.Evaluate |
| PUnifyLog | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PunInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pureTerm | Idris.Core.TT |
| pushIndent | Idris.ParseHelpers, Idris.Parser |
| putIState | Idris.AbsSyntax |
| PVar | Idris.Core.TT |
| pvars | Idris.ElabDecls |
| PVTy | Idris.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 | Idris.Core.ProofState, Idris.Core.Elaborate |
| Qed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| qed | Idris.Core.Elaborate |
| qelem | Idris.Coverage |
| qshow | Idris.Core.Elaborate |
| quickEq | Idris.Coverage |
| Quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quit | |
| 1 (Data Constructor) | Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quote | Idris.Core.Evaluate |
| quote | Idris.Core.Evaluate |
| quoteGoal | Idris.ParseExpr, Idris.Parser |
| RApp | Idris.Core.TT |
| Raw | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| rawBool | Idris.ElabTerm |
| rawCons | Idris.ElabTerm |
| rawList | Idris.ElabTerm |
| rawNil | Idris.ElabTerm |
| RawOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| rawPair | Idris.ElabTerm |
| rawPairTy | Idris.ElabTerm |
| raw_apply | Idris.Core.TT |
| raw_unapply | Idris.Core.TT |
| RBind | Idris.Core.TT |
| RConstant | Idris.Core.TT |
| REBASE | IRTS.Bytecode |
| receiveInput | Idris.Prover |
| recheck | Idris.Core.Typecheck |
| recheckC | Idris.ElabDecls |
| record | Idris.ParseData, Idris.Parser |
| recordType | Idris.ParseExpr, Idris.Parser |
| recursive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ref | Idris.Core.TT |
| Refine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflCall | Idris.ElabTerm |
| Reflect | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflect | Idris.ElabTerm |
| reflectBinder | Idris.ElabTerm |
| reflectConstant | Idris.ElabTerm |
| reflectCtxt | Idris.ElabTerm |
| reflectEnv | Idris.ElabTerm |
| reflectErr | Idris.ElabTerm |
| reflectFunctionErrors | Idris.ElabTerm |
| Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ReflectionError | Idris.Core.TT |
| ReflectionFailed | Idris.Core.TT |
| reflectName | Idris.ElabTerm |
| reflectNameType | Idris.ElabTerm |
| reflectUExp | Idris.ElabTerm |
| reflErrName | Idris.ElabTerm |
| reflm | Idris.ElabTerm |
| Reg | |
| 1 (Type/Class) | IRTS.BCImp |
| 2 (Type/Class) | IRTS.Bytecode |
| Regret | Idris.Core.ProofState, Idris.Core.Elaborate |
| regret | Idris.Core.Elaborate |
| reify | Idris.ElabTerm |
| reifyApp | Idris.ElabTerm |
| reifyRaw | Idris.ElabTerm |
| reifyRawApp | Idris.ElabTerm |
| reifyReportPart | 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 |
| renderWidth | Idris.AbsSyntax |
| Reorder | Idris.Core.ProofState, Idris.Core.Elaborate |
| reorder_claims | Idris.Core.Elaborate |
| repl | Idris.REPL |
| replaceSplits | Idris.CaseSplit |
| replCompletion | Idris.Completion |
| REPLCompletions | Idris.IdeSlave |
| replPkg | Pkg.Package |
| replSettings | Idris.REPL |
| report | Idris.Error |
| RESERVE | IRTS.Bytecode |
| reserved | Idris.ParseHelpers, Idris.Parser |
| reservedOp | Idris.ParseHelpers, Idris.Parser |
| resetNameIdx | Idris.AbsSyntax |
| resolveProof | Idris.REPL |
| resolveTC | Idris.ElabTerm |
| Rewrite | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| rewrite | Idris.Core.Elaborate |
| rewriteTerm | Idris.ParseExpr, Idris.Parser |
| RForce | Idris.Core.TT |
| rhs | Idris.Parser |
| RightOK | Idris.AbsSyntax |
| rmIBC | Pkg.Package |
| RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RType | Idris.Core.TT |
| rt_simplify | Idris.Core.Evaluate |
| Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| runClient | Idris.REPL |
| runElab | Idris.Core.Elaborate |
| runInnerParser | Idris.ParseHelpers, Idris.Parser |
| runIO | Idris.AbsSyntax |
| runparser | Idris.ParseHelpers, Idris.Parser |
| runTac | Idris.ElabTerm |
| RunTime | Idris.Core.CaseTree |
| runtimeExceptionType | IRTS.Java.JTypes |
| RVal | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | IRTS.Bytecode |
| safeToEnum | Idris.IBC |
| SAlt | IRTS.Simplified |
| sAlt | IRTS.Simplified |
| Same | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SApp | IRTS.Simplified |
| saveState | Idris.Core.Elaborate |
| SC | Idris.Core.CaseTree |
| SC' | Idris.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 | Idris.Core.TT |
| SDecl | IRTS.Simplified |
| SDefaultCase | IRTS.Simplified |
| Search | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| serialize | IRTS.DumpBC |
| serializeBC | IRTS.DumpBC |
| serializeCase | IRTS.DumpBC |
| serializeDefault | IRTS.DumpBC |
| serializeReg | IRTS.DumpBC |
| SError | IRTS.Simplified |
| setAccess | Idris.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 |
| SetConsoleWidth | Idris.AbsSyntaxTree, 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 | Idris.Core.Elaborate |
| SetInjective | Idris.Core.ProofState, Idris.Core.Elaborate |
| setLogLevel | Idris.AbsSyntax |
| setMetaInformation | Idris.Core.Evaluate |
| setNextName | Idris.Core.Elaborate |
| setNoBanner | Idris.AbsSyntax |
| SetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| setOptLevel | Idris.AbsSyntax |
| setOutH | Idris.AbsSyntax |
| setOutputTy | Idris.AbsSyntax |
| setQuiet | Idris.AbsSyntax |
| setREPL | Idris.AbsSyntax |
| setShowOrigErr | Idris.AbsSyntax |
| setSO | Idris.AbsSyntax |
| setTargetCPU | Idris.AbsSyntax |
| setTargetTriple | Idris.AbsSyntax |
| setTotal | Idris.Core.Evaluate |
| setTotality | Idris.AbsSyntax |
| setTypeCase | Idris.AbsSyntax |
| setTypeInType | Idris.AbsSyntax |
| setVerbose | Idris.AbsSyntax |
| setWidth | Idris.AbsSyntax |
| set_context | Idris.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 |
| showCaseTrees | IRTS.Compiler |
| showCG | Idris.Core.TT |
| showCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDeclImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDecls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDoc | Idris.Docs |
| showEnv | Idris.Core.TT |
| showEnv' | Idris.Core.TT |
| showEnvDbg | Idris.Core.TT |
| showErr | Idris.Error |
| ShowImpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowIncs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowLibdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowLibs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ShowOrigErr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showOrigErr | Idris.AbsSyntax |
| ShowProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showProof | Idris.Prover |
| showSep | Idris.Core.TT |
| showTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showTmImpls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showTotal | Idris.REPL |
| showTotalN | Idris.REPL |
| sigmaTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| simpleCase | Idris.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 | Idris.Core.Elaborate |
| Simplify | Idris.Core.ProofState, Idris.Core.Elaborate |
| simplify | |
| 1 (Function) | Idris.Core.Evaluate |
| 2 (Function) | IRTS.Simplified |
| 3 (Function) | Idris.Core.Elaborate |
| simplifyCasedef | Idris.Core.Evaluate |
| singleLineComment | Idris.ParseHelpers, Idris.Parser |
| sInstanceN | Idris.Core.TT |
| SizeChange | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SLet | IRTS.Simplified |
| SLIDE | IRTS.Bytecode |
| small | Idris.Core.CaseTree |
| Smaller | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| sMN | Idris.Core.TT |
| SN | Idris.Core.TT |
| sname | |
| 1 (Function) | IRTS.Compiler |
| 2 (Function) | Idris.Transforms |
| SNothing | IRTS.Simplified |
| sNS | Idris.Core.TT |
| Solve | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| solve | Idris.Core.Elaborate |
| solveAll | Idris.ElabTerm |
| solved | Idris.Core.ProofState, Idris.Core.Elaborate |
| solveDeferred | Idris.AbsSyntax |
| SOp | IRTS.Simplified |
| sourcefile | Idris.IBC |
| sourceTypes | IRTS.Java.JTypes |
| sParentN | Idris.Core.TT |
| Spec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SpecialHeaderArg | Idris.Help |
| Specialise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| specialise | Idris.Core.Evaluate |
| SpecialName | Idris.Core.TT |
| specType | Idris.PartialEval |
| splitOnLine | Idris.CaseSplit |
| SProj | IRTS.Simplified |
| srcPath | Idris.Imports |
| SSymbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| startServer | Idris.REPL |
| StartUnify | Idris.Core.ProofState, Idris.Core.Elaborate |
| start_unify | Idris.Core.Elaborate |
| Static | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| static | Idris.ParseExpr, Idris.Parser |
| STerm | Idris.Core.CaseTree |
| STOREOLD | IRTS.Bytecode |
| Str | Idris.Core.TT |
| str | Idris.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 | Idris.Core.TT |
| SubReport | Idris.Core.TT |
| subst | Idris.Core.TT |
| substMatch | Idris.AbsSyntax |
| substMatches | Idris.AbsSyntax |
| substMatchesShadow | Idris.AbsSyntax |
| substMatchShadow | Idris.AbsSyntax |
| substNames | Idris.Core.TT |
| substTerm | Idris.Core.TT |
| substV | Idris.Core.TT |
| suc | Idris.Transforms |
| SucCase | Idris.Core.CaseTree |
| sUN | Idris.Core.TT |
| SUpdate | IRTS.Simplified |
| SV | IRTS.Simplified |
| sVar | IRTS.Simplified |
| Symbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| symbol | Idris.ParseHelpers, Idris.Parser |
| SymbolAtom | Idris.IdeSlave |
| symbols | Idris.IBC |
| SymRef | Idris.Core.TT |
| 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 | Idris.Core.Elaborate |
| TacImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacimpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Tactic | Idris.Core.ProofState, Idris.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 | Idris.Core.TT |
| TC' | Idris.Core.TC, Idris.Core.TT |
| TCInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tclift | Idris.Error |
| tcname | Idris.Core.TT |
| TCon | Idris.Core.TT |
| tctry | Idris.Error |
| tc_dictionary | Idris.Core.Evaluate |
| Term | Idris.Core.TT |
| terminator | Idris.ParseHelpers, Idris.Parser |
| TermPart | Idris.Core.TT |
| TermSize | Idris.Core.TT |
| termsize | Idris.Core.TT |
| TermSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TermTrans | Idris.Transforms |
| TestInline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| testLib | Pkg.Package |
| TextPart | Idris.Core.TT |
| tfail | Idris.Core.TT |
| thead | Idris.Core.TT |
| Theorem | Idris.Core.Elaborate |
| thname | Idris.Core.ProofState, Idris.Core.Elaborate |
| threadType | IRTS.Java.JTypes |
| TI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| timestampOlder | Idris.IBC |
| tldeclared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Tmp | IRTS.Bytecode |
| tnull | Idris.Core.TT |
| toAlist | Idris.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 |
| TooManyArguments | Idris.Core.TT |
| TOPBASE | IRTS.Bytecode |
| toplevel | Idris.ElabTerm |
| toRefType | IRTS.Java.ASTBuilding |
| toSExp | Idris.IdeSlave |
| toTable | Idris.ParseOps, Idris.Parser |
| Total | Idris.Core.Evaluate |
| TotalFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Totality | Idris.Core.Evaluate |
| totality | Idris.Parser |
| TotCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| totcheck | Idris.AbsSyntax |
| TRACE | IRTS.CodegenCommon |
| traceUnused | Idris.UnusedArgs |
| traceWhen | Idris.Core.TT |
| Transform | Idris.Transforms |
| transform | |
| 1 (Function) | Idris.Parser |
| 2 (Function) | Idris.Transforms |
| Trivial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| trivial | Idris.ProofSearch |
| trivial' | Idris.ElabTerm |
| trun | Idris.Core.TT |
| Try | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| try | Idris.Core.Elaborate |
| try' | Idris.Core.Elaborate |
| tryAll | Idris.Core.Elaborate |
| tryLoadLib | Util.DynamicLinker |
| tryWhen | Idris.Core.Elaborate |
| TSeq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TT | Idris.Core.TT |
| TTOpt | Idris.Transforms |
| TType | Idris.Core.TT |
| TTypeInTType | Idris.Core.TT |
| tt_ctxt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| txt | Idris.Core.TT |
| TyDecl | Idris.Core.Evaluate |
| tyOptDeclList | Idris.ParseExpr, Idris.Parser |
| Type | Idris.Core.TT |
| type1Doc | Idris.AbsSyntax |
| 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 |
| TypeOrTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TypeOutput | Idris.Core.TT |
| TypeProviders | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ucheck | Idris.Core.Constraints |
| UConstraint | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| uconstraints | Idris.Core.Evaluate |
| UCs | Idris.Core.TT |
| UExp | Idris.Core.TT |
| UImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ULE | Idris.Core.TT |
| ULT | Idris.Core.TT |
| UN | Idris.Core.TT |
| unApply | Idris.Core.TT |
| Unchecked | Idris.Core.Evaluate |
| Unconditional | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| underline | Idris.Colours |
| Undo | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| undo | Idris.Core.Elaborate |
| unIdiom | Idris.DSL |
| unified | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifiedD | Idris.PartialEval |
| unify | Idris.Core.Unify |
| unifyLog | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| unifylog | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifyProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyProblems | Idris.Core.Elaborate |
| UnifyScope | Idris.Core.TT |
| uniqueBinders | Idris.Core.TT |
| uniqueName | Idris.Core.TT |
| uniqueNameCtxt | Idris.Core.Evaluate |
| uniqueNameFrom | Idris.Core.TT |
| unique_hole | Idris.Core.Elaborate |
| unique_hole' | Idris.Core.Elaborate |
| unitCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UniverseError | Idris.Core.TT |
| Universes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Unknown | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unList | Idris.Core.TT |
| unlit | Idris.Unlit |
| UnmatchedCase | Idris.Core.CaseTree |
| UnsetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unusedpos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unwrapFC | Idris.Core.TT |
| upd | Idris.Coverage |
| UPDATE | IRTS.Bytecode |
| updateAux | Idris.Core.Elaborate |
| updateContext | Idris.AbsSyntax |
| updateDef | Idris.Core.TT |
| updateN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updateNs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| update_term | Idris.Core.Elaborate |
| Usage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UseCodegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| used | Idris.UnusedArgs |
| usedArg | IRTS.Lang, IRTS.Defunctionalise |
| usedIn | IRTS.Lang, IRTS.Defunctionalise |
| usedNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedns | Idris.Core.ProofState, Idris.Core.Elaborate |
| useREPL | Idris.AbsSyntax |
| UseUndef | Idris.Core.Evaluate |
| Using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usingDecl | Idris.Parser |
| usingDeclList | Idris.Parser |
| using_ | Idris.Parser |
| UVal | Idris.Core.TT |
| UVar | Idris.Core.TT |
| V | Idris.Core.TT |
| valIBCSubDir | Idris.AbsSyntax |
| Value | Idris.Core.Evaluate |
| VApp | Idris.Core.Evaluate |
| Var | Idris.Core.TT |
| var | Idris.DSL |
| VBind | Idris.Core.Evaluate |
| VBLet | Idris.Core.Evaluate |
| VConstant | Idris.Core.Evaluate |
| Ver | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ver | |
| 1 (Function) | Idris.IBC |
| 2 (Function) | Idris.REPL |
| VErased | Idris.Core.Evaluate |
| verbatimStringLiteral | Idris.ParseExpr, Idris.Parser |
| Verbose | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| verbose | Idris.AbsSyntax |
| 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 | Idris.Core.Evaluate |
| vinstances | Idris.Core.TT |
| vivid | Idris.Colours |
| VoidType | Idris.Core.TT |
| voidType | IRTS.Java.JTypes |
| VP | Idris.Core.Evaluate |
| VProj | Idris.Core.Evaluate |
| VTmp | Idris.Core.Evaluate |
| vToP | Idris.Core.TT |
| VType | Idris.Core.Evaluate |
| VV | Idris.Core.Evaluate |
| WarnOnly | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| WarnPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| weakenEnv | Idris.Core.TT |
| weakenTm | Idris.Core.TT |
| weakenTmEnv | Idris.Core.TT |
| wExpr | Idris.Parser |
| whereBlock | Idris.Parser |
| WhereN | Idris.Core.TT |
| whiteSpace | Idris.ParseHelpers, Idris.Parser |
| withErrorReflection | Idris.ElabTerm |
| Wk | Idris.Core.TT |
| WkEnv | Idris.Core.TT |
| WkEnvTT | Idris.Core.TT |
| writeIBC | Idris.IBC |
| zero | Idris.Transforms |
| zname | |
| 1 (Function) | IRTS.Compiler |
| 2 (Function) | Idris.Transforms |
| ~&&~ | IRTS.Java.ASTBuilding |
| ~==~ | IRTS.Java.ASTBuilding |
| ~> | IRTS.Java.ASTBuilding |