Index
| Abandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| accData | Idris.ParseHelpers, Idris.Parser |
| Accessibility | Idris.Core.Evaluate |
| accessibility | Idris.ParseHelpers, Idris.Parser |
| addAcc | Idris.ParseHelpers, Idris.Parser |
| addAlist | Idris.Core.TT |
| addApps | IRTS.Defunctionalise |
| addAutoImport | Idris.AbsSyntax |
| addBinder | Idris.Core.TT |
| addCasedef | Idris.Core.Evaluate |
| addClass | Idris.AbsSyntax |
| AddClause | Idris.IdeMode |
| AddClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addClauseFrom | Idris.Interactive |
| addCoercion | Idris.AbsSyntax |
| addConstraints | Idris.AbsSyntax |
| addCtxtDef | Idris.Core.Evaluate |
| addDatatype | Idris.Core.Evaluate |
| addDef | Idris.Core.TT |
| addDeferred | Idris.AbsSyntax |
| addDeferred' | Idris.AbsSyntax |
| addDeferredTyCon | Idris.AbsSyntax |
| addDocStr | Idris.AbsSyntax |
| addDyLib | Idris.AbsSyntax |
| addErasureUsage | Idris.AbsSyntax |
| addErrRev | Idris.AbsSyntax |
| addExport | Idris.AbsSyntax |
| addFlag | Idris.AbsSyntax |
| addFn | IRTS.Lang, IRTS.Defunctionalise |
| addFunctionErrorHandlers | Idris.AbsSyntax |
| addHdr | Idris.AbsSyntax |
| addHides | Idris.Parser |
| addIBC | Idris.AbsSyntax |
| addImpl | Idris.AbsSyntax |
| addImpl' | Idris.AbsSyntax |
| addImplBound | Idris.AbsSyntax |
| addImplBoundInf | Idris.AbsSyntax |
| addImplPat | Idris.AbsSyntax |
| addImportDir | Idris.AbsSyntax |
| addImported | Idris.AbsSyntax |
| addInstance | Idris.AbsSyntax |
| addInternalApp | Idris.AbsSyntax |
| addLangExt | Idris.AbsSyntax |
| addLib | Idris.AbsSyntax |
| AddMissing | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| addMissing | Idris.Interactive |
| addNameHint | Idris.AbsSyntax |
| addNameIdx | Idris.AbsSyntax |
| addNameIdx' | Idris.AbsSyntax |
| addObjectFile | Idris.AbsSyntax |
| addOperator | Idris.Core.Evaluate |
| AddOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addOptimise | Idris.AbsSyntax |
| AddProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AddProofClause | Idris.IdeMode |
| AddProofClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| addProofClauseFrom | Idris.Interactive |
| addReplSyntax | Idris.Parser |
| addStatics | Idris.AbsSyntax |
| addSyntax | Idris.Parser |
| addTags | IRTS.Lang, IRTS.Defunctionalise |
| addToCalledG | Idris.AbsSyntax |
| addToCG | Idris.AbsSyntax |
| addToCtxt | Idris.Core.Evaluate |
| ADDTOP | IRTS.Bytecode |
| addToUsing | Idris.AbsSyntax |
| addTrans | Idris.AbsSyntax |
| addTyDecl | Idris.Core.Evaluate |
| addTyInfConstraints | Idris.AbsSyntax |
| addTyInferred | Idris.AbsSyntax |
| addUsedName | Idris.AbsSyntax |
| addUsingConstraints | Idris.AbsSyntax |
| addUsingImpls | Idris.AbsSyntax |
| aiFn | Idris.AbsSyntax |
| allHelp | Idris.REPLParser |
| allImportDirs | Idris.AbsSyntax |
| allNames | Idris.AbsSyntax |
| allNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| allNothing | Idris.Coverage |
| allocUnique | IRTS.Lang, IRTS.Defunctionalise |
| allowImp | Idris.ParseExpr, Idris.Parser |
| allTTNames | Idris.Core.TT |
| AllTypes | Idris.Core.TT |
| AlreadyDefined | Idris.Core.TT |
| alt | Idris.ParseExpr, Idris.Parser |
| AltsTArg | Idris.ParseExpr, Idris.Parser |
| AlwaysShow | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AnnBoundName | Idris.Core.TT |
| AnnConst | Idris.Core.TT |
| AnnData | Idris.Core.TT |
| AnnErr | Idris.Core.TT |
| AnnFC | Idris.Core.TT |
| AnnKeyword | Idris.Core.TT |
| AnnName | Idris.Core.TT |
| annName | Idris.Delaborate |
| annotCode | Idris.Docstrings |
| AnnSearchResult | Idris.Core.TT |
| AnnTerm | Idris.Core.TT |
| AnnTextFmt | Idris.Core.TT |
| AnnType | Idris.Core.TT |
| AnySyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| App | Idris.Core.TT |
| app | Idris.ParseExpr, Idris.Parser |
| apply | Idris.Core.Elaborate |
| apply' | Idris.Core.Elaborate |
| apply2 | Idris.Core.Elaborate |
| ApplyCase | IRTS.Defunctionalise |
| applyDataOptRT | Idris.DataOpts |
| applyOpts | Idris.DataOpts |
| ApplyTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| applyTransRules | Idris.Transforms |
| applyTransRulesWith | Idris.Transforms |
| apply_elab | Idris.Core.Elaborate |
| Apropos | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| apropos | Idris.Apropos |
| aproposModules | Idris.Apropos |
| arg | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| argExpr | Idris.Parser |
| argName | Idris.Reflection |
| ArgOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsdef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argsused | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argTy | Idris.Reflection |
| ArithTy | Idris.Core.TT |
| arity | Idris.Core.TT |
| AssertTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ASSIGN | IRTS.Bytecode |
| assign | IRTS.Bytecode |
| ASSIGNCONST | IRTS.Bytecode |
| assumptionNames | Idris.Prover |
| At | Idris.Core.TT |
| ATFloat | Idris.Core.TT |
| atHole | Idris.Core.ProofTerm |
| ATInt | Idris.Core.TT |
| Attack | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| attack | Idris.Core.Elaborate |
| AType | Idris.Core.TT |
| AutoArg | Idris.Core.ProofState, Idris.Core.Elaborate |
| autoArg | Idris.Core.Elaborate |
| AutomaticWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| autos | Idris.Core.ProofState, Idris.Core.Elaborate |
| AutoSolve | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AutoWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| binary | Idris.ParseOps, Idris.Parser |
| Bind | Idris.Core.TT |
| bindAll | Idris.Core.TT |
| Binder | Idris.Core.TT |
| binderImpl | Idris.Core.TT |
| binderKind | Idris.Core.TT |
| binderTy | Idris.Core.TT |
| binderVal | Idris.Core.TT |
| Binding | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bindingOf | Idris.Core.TT |
| bindList | Idris.ParseHelpers, Idris.Parser |
| bindsymbol | Idris.ParseExpr, Idris.Parser |
| bindTC | Idris.Core.TT |
| bindTyArgs | Idris.Core.TT |
| Block | Idris.Docstrings |
| Blockquote | Idris.Docstrings |
| bold | Idris.Colours |
| BoldText | Idris.Core.TT |
| BoolAtom | Idris.IdeMode |
| Bound | Idris.Core.TT |
| boundNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| BoundVarColour | Idris.Colours |
| boundVarColour | Idris.Colours |
| bound_in | Idris.Core.ProofTerm |
| bound_in_term | Idris.Core.ProofTerm |
| brace_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| bracketed | Idris.ParseExpr, Idris.Parser |
| bracketed' | Idris.ParseExpr, Idris.Parser |
| bracketedExpr | Idris.ParseExpr, Idris.Parser |
| BufferType | Idris.Core.TT |
| bugaddr | Idris.Delaborate |
| build | Idris.ElabTerm |
| buildMods | Pkg.Package |
| buildPkg | Pkg.Package |
| buildSCG | Idris.Coverage |
| buildSCG' | Idris.Coverage |
| buildTC | Idris.ElabTerm |
| buildTree | Idris.Chaser |
| buildType | Idris.Elab.Type |
| ByReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Bytecode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| caf | Idris.Parser |
| calcProd | Idris.Coverage |
| calcTotality | Idris.Coverage |
| CALL | IRTS.Bytecode |
| calls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CallsWho | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| callsWho | Idris.WhoCalls |
| canBeDConName | Idris.Core.Evaluate |
| CantConvert | Idris.Core.TT |
| CantInferType | Idris.Core.TT |
| CantIntroduce | Idris.Core.TT |
| CantMatch | 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 |
| caseSensitive | Idris.Imports |
| CaseSplit | Idris.IdeMode |
| CaseSplitAt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| caseSplitAt | Idris.Interactive |
| cases_compiletime | Idris.Core.Evaluate |
| cases_inlined | Idris.Core.Evaluate |
| cases_runtime | Idris.Core.Evaluate |
| cases_totcheck | Idris.Core.Evaluate |
| CaseTac | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| casetac | Idris.Core.Elaborate |
| CaseTree | Idris.Core.CaseTree |
| CaseType | Idris.Core.CaseTree |
| case_ | Idris.ElabTerm |
| case_alwaysinline | Idris.Core.Evaluate |
| case_decls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| case_inlinable | Idris.Core.Evaluate |
| catchError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| catchIO | Util.System |
| CExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CGInfo | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| cg_usedpos | Idris.ASTUtils |
| Ch | Idris.Core.TT |
| ChangeDirectory | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| char | Idris.ParseHelpers, Idris.Parser |
| charLiteral | Idris.ParseHelpers, Idris.Parser |
| Check | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| check | Idris.Core.Typecheck |
| check' | Idris.Core.Typecheck |
| checkAddDef | Idris.Elab.Utils |
| checkAllCovering | Idris.Coverage |
| CheckConv | Idris.Core.TT |
| checkDeclTotality | Idris.Coverage |
| checkDef | Idris.Elab.Utils |
| checkDocs | Idris.Elab.Utils |
| checkDocstring | Idris.Docstrings |
| checkDSL | Idris.ParseData, Idris.Parser |
| Checked | Idris.Docstrings |
| CheckIn | Idris.Core.ProofState, Idris.Core.Elaborate |
| checkInferred | Idris.Elab.Utils |
| checkInjective | Idris.Core.Elaborate |
| checkMP | Idris.Coverage |
| checkPiGoal | Idris.Core.Elaborate |
| checkPkg | Pkg.Package |
| checkPositive | Idris.Coverage |
| checkPossible | Idris.Elab.Clause |
| checkSizeChange | Idris.Coverage |
| checkTotality | Idris.Coverage |
| checkUndefined | Idris.AbsSyntax |
| checkUnique | Idris.Core.Typecheck |
| check_in | Idris.Core.Elaborate |
| CI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Claim | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| claim | Idris.Core.Elaborate |
| ClaimFn | Idris.Core.ProofState, Idris.Core.Elaborate |
| claimFn | Idris.Core.Elaborate |
| claimTT | Idris.ElabTerm |
| classBlock | Idris.Parser |
| ClassDoc | Idris.Docs |
| ClassInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_ | Idris.Parser |
| class_defaults | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_default_superclasses | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| class_determiners | 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 |
| clearParserWarnings | Idris.ParseHelpers, Idris.Parser |
| clearPTypes | Idris.AbsSyntax |
| clear_totcheck | Idris.AbsSyntax |
| Client | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| closeBlock | Idris.ParseHelpers, Idris.Parser |
| CmdArg | Idris.Help |
| cmdOptType | Idris.AbsSyntax |
| Codata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Code | Idris.Docstrings |
| CodeBlock | Idris.Docstrings |
| Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegen | Idris.AbsSyntax |
| codegenC | IRTS.CodegenC |
| CodeGenerator | IRTS.CodegenCommon |
| CodegenInfo | |
| 1 (Type/Class) | IRTS.CodegenCommon |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| codegenJavaScript | IRTS.CodegenJavaScript |
| codegenNode | IRTS.CodegenJavaScript |
| codegen_ | Idris.Parser |
| Coinductive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| collapse | Idris.Coverage |
| collapse' | Idris.Coverage |
| collapseNothing | Idris.Coverage |
| collect | Idris.ParseHelpers, Idris.Parser |
| collectDeferred | Idris.ElabTerm |
| colour | Idris.Colours |
| ColourArg | Idris.Help |
| colourise | |
| 1 (Function) | Idris.Colours |
| 2 (Function) | Idris.AbsSyntax |
| colouriseBound | Idris.Colours |
| colouriseData | Idris.Colours |
| colouriseFun | Idris.Colours |
| colouriseImplicit | Idris.Colours |
| colouriseKeyword | Idris.Colours |
| colouriseKwd | Idris.Colours |
| colourisePostulate | 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 | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| commentMarkers | Idris.ParseHelpers, Idris.Parser |
| Compile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compile | IRTS.Compiler |
| compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compileJS | IRTS.JavaScript.AST |
| compileJS' | IRTS.JavaScript.AST |
| compileLibs | IRTS.CodegenCommon |
| compileObjs | IRTS.CodegenCommon |
| compilerFlags | IRTS.CodegenCommon |
| CompileTime | Idris.Core.CaseTree |
| CompleteFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| complete_fill | Idris.Core.Elaborate |
| 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 |
| consoleDecorate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| consoleDisplayAnnotated | Idris.Output |
| ConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ConsoleWidthArg | Idris.Help |
| Const | Idris.Core.TT |
| constAlt | IRTS.Bytecode |
| Constant | Idris.Core.TT |
| constant | Idris.ParseExpr, Idris.Parser |
| constants | Idris.ParseExpr, Idris.Parser |
| CONSTCASE | IRTS.Bytecode |
| ConstCase | Idris.Core.CaseTree |
| constCase | IRTS.Bytecode |
| constDocs | Idris.Core.TT |
| constIsType | Idris.Core.TT |
| Constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraintArg | Idris.ParseExpr, Idris.Parser |
| ConstraintFC | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.Core.TT |
| constraintList | Idris.ParseExpr, Idris.Parser |
| constraintList1 | Idris.ParseExpr, Idris.Parser |
| Constructor | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constructor | Idris.ParseData, Idris.Parser |
| containsHole | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| containsText | Idris.Docstrings |
| Context | Idris.Core.Evaluate |
| context | Idris.Core.ProofState, Idris.Core.Elaborate |
| convEq | Idris.Core.Evaluate |
| convEq' | Idris.Core.Evaluate |
| converts | Idris.Core.Typecheck |
| convertsC | Idris.Core.Typecheck |
| convSExp | Idris.IdeMode |
| con_names | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Core | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| coverage | Idris.AbsSyntax |
| CoveringFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ctxt | Idris.Core.TT |
| ctxtAlist | Idris.Core.Evaluate |
| ctxt_lookup | Idris.ASTUtils |
| 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 |
| debugElaborator | Idris.Core.Elaborate |
| DebugInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| debugLevel | IRTS.CodegenCommon |
| DebugUnify | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| decl | Idris.Parser |
| decl' | Idris.Parser |
| declare | IRTS.Defunctionalise |
| declared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DeclArg | Idris.Help |
| decorateid | Idris.Elab.Utils |
| decoration | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Def | Idris.Core.Evaluate |
| defaultAlt | IRTS.Bytecode |
| DefaultCase | Idris.Core.CaseTree |
| DefaultCaseFun | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DefaultEliminator | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultOptimise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DefaultPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultPort | Idris.REPL |
| defaultPPOption | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultScoreFunction | Idris.TypeSearch |
| 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 |
| definitions | Idris.Core.Evaluate |
| Defn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defunctionalise | IRTS.Defunctionalise |
| defunDecls | IRTS.CodegenCommon |
| delab | Idris.Delaborate |
| delab' | Idris.Delaborate |
| delabMV | Idris.Delaborate |
| delabTy | Idris.Delaborate |
| delabTy' | Idris.Delaborate |
| delayed_elab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| delazy | Idris.Coverage |
| delazy' | Idris.Coverage |
| deleteDefExact | Idris.Core.TT |
| DError | IRTS.Defunctionalise |
| desugar | Idris.DSL |
| desugarAs | Idris.Elab.AsPat |
| detaggable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| docComment | Idris.ParseHelpers, Idris.Parser |
| Docs | Idris.Docs |
| Docs' | Idris.Docs |
| DocsFor | Idris.IdeMode |
| DocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DocString | Idris.Docstrings |
| Docstring | Idris.Docstrings |
| docstring | Idris.Parser |
| DocTerm | Idris.Docstrings |
| documentPkg | Pkg.Package |
| doesDirectoryExist' | Idris.Imports |
| doesFileExist' | Idris.Imports |
| DoExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| doInline | IRTS.LangOpts |
| DoLet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DoLetP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| done | Idris.Core.ProofState, Idris.Core.Elaborate |
| doneElaboratingAppPS | Idris.Core.ProofState, Idris.Core.Elaborate |
| doneElaboratingArgPS | Idris.Core.ProofState, Idris.Core.Elaborate |
| done_elaborating_app | Idris.Core.Elaborate |
| done_elaborating_arg | Idris.Core.Elaborate |
| dontunify | Idris.Core.ProofState, Idris.Core.Elaborate |
| DOp | IRTS.Defunctionalise |
| DoProofSearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| doProofSearch | Idris.Interactive |
| dotted | Idris.Core.ProofState, Idris.Core.Elaborate |
| dotterm | Idris.Core.Elaborate |
| DoUnify | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| do_ | Idris.ParseExpr, Idris.Parser |
| do_alt | 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 |
| dslify | Idris.DSL |
| 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_pi | 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 |
| DumpDefun | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dumpDefuns | IRTS.Defunctionalise |
| 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 |
| d_unique | Idris.Core.TT |
| EAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EDefns | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Edit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| edit | Idris.REPL |
| eEVAL | IRTS.Defunctionalise |
| EInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eInfoNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EitherErr | Idris.AbsSyntax |
| Elab | Idris.Core.Elaborate |
| elab | Idris.ElabTerm |
| Elab' | Idris.Core.Elaborate |
| elabCaseBlock | Idris.Elab.Utils |
| elabClass | Idris.Elab.Class |
| elabClause | Idris.Elab.Clause |
| elabClauses | Idris.Elab.Clause |
| ElabCtxt | |
| 1 (Type/Class) | Idris.ElabTerm |
| 2 (Data Constructor) | Idris.ElabTerm |
| ElabD | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elabData | Idris.Elab.Data |
| ElabDebug | Idris.Core.TT |
| elabDecl | Idris.ElabDecls |
| elabDecl' | Idris.ElabDecls |
| elabDecls | Idris.ElabDecls |
| elabDocTerms | Idris.Elab.Value |
| elabFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ElabInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elabInstance | Idris.Elab.Instance |
| elabMain | Idris.ElabDecls |
| ElabMode | Idris.ElabTerm |
| elaborate | Idris.Core.Elaborate |
| Elaborating | Idris.Core.TT |
| ElaboratingArg | Idris.Core.TT |
| elaboratingArgErr | Idris.ElabTerm |
| elaborating_app | Idris.Core.Elaborate |
| elabPE | Idris.Elab.Clause |
| elabPostulate | Idris.Elab.Type |
| elabPrims | Idris.ElabDecls |
| elabProvider | Idris.Elab.Provider |
| elabRecord | Idris.Elab.Record |
| ElabResult | |
| 1 (Type/Class) | Idris.ElabTerm |
| 2 (Data Constructor) | Idris.ElabTerm |
| ElabState | Idris.Core.Elaborate |
| elabStep | Idris.Prover |
| elabTransform | Idris.Elab.Transform |
| elabType | Idris.Elab.Type |
| elabType' | Idris.Elab.Type |
| elabVal | Idris.Elab.Value |
| elabValBind | Idris.Elab.Value |
| ElabWhat | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elab_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ELHS | Idris.ElabTerm |
| ElimN | Idris.Core.TT |
| elog | Idris.Core.Elaborate |
| Emph | Idris.Docstrings |
| emptyContext | Idris.Core.TT |
| emptyDocstring | Idris.Docstrings |
| emptyFC | Idris.Core.TT |
| EmptyMI | Idris.Core.Evaluate |
| emptySyntaxRules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Endianness | IRTS.Lang, IRTS.Defunctionalise |
| EndUnify | Idris.Core.ProofState, Idris.Core.Elaborate |
| end_unify | Idris.Core.Elaborate |
| Entity | Idris.Docstrings |
| 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 |
| eqDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqParamDoc | 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 |
| ErasureInfo | Idris.Core.CaseTree |
| ERHS | Idris.ElabTerm |
| Err | Idris.Core.TT |
| Err' | Idris.Core.TT |
| errAt | Idris.Core.Elaborate |
| ErrContext | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| errContext | Idris.AbsSyntax |
| errEnv | Idris.Core.Typecheck |
| ERROR | IRTS.Bytecode |
| Error | Idris.Core.TT |
| ErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ErrorReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ErrorReportPart | Idris.Core.TT |
| ErrorReverse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ErrPPrint | Idris.IdeMode |
| errReverse | Idris.ErrReverse |
| errSpan | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ErrString | Idris.IdeMode |
| erun | Idris.Core.Elaborate |
| ES | Idris.Core.Elaborate |
| EState | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ETyDecl | Idris.ElabTerm |
| ETypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Eval | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EvalApply | IRTS.Defunctionalise |
| EvalCase | IRTS.Defunctionalise |
| evalD | IRTS.Inliner |
| EvalExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| Example | Idris.Docstrings |
| 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 |
| ExpectedType | Idris.Core.TT |
| 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 |
| Export | |
| 1 (Data Constructor) | IRTS.Lang, IRTS.Defunctionalise |
| 2 (Type/Class) | IRTS.Lang, IRTS.Defunctionalise |
| ExportData | IRTS.Lang, IRTS.Defunctionalise |
| exportDecls | IRTS.CodegenCommon |
| ExportFun | IRTS.Lang, IRTS.Defunctionalise |
| ExportIFace | IRTS.Lang, IRTS.Defunctionalise |
| Expr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expr | Idris.ParseExpr, Idris.Parser |
| expr' | Idris.ParseExpr, Idris.Parser |
| ExprArg | Idris.Help |
| ExprTArg | Idris.ParseExpr, Idris.Parser |
| Extension | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| extension | Idris.ParseExpr, Idris.Parser |
| extensions | Idris.ParseExpr, Idris.Parser |
| externalExpr | Idris.ParseExpr, Idris.Parser |
| ExternalIO | Idris.Core.Evaluate |
| extractUnquotes | Idris.ElabQuasiquote |
| extraHelp | Idris.Help |
| e_guarded | Idris.ElabTerm |
| e_inarg | Idris.ElabTerm |
| e_intype | Idris.ElabTerm |
| e_isfn | Idris.ElabTerm |
| e_nomatching | Idris.ElabTerm |
| e_qq | Idris.ElabTerm |
| FailAt | Idris.Core.Unify |
| FailContext | |
| 1 (Type/Class) | Idris.Core.Unify |
| 2 (Data Constructor) | Idris.Core.Unify |
| Failing | Idris.Docstrings |
| failMsg | Idris.Core.TT |
| Fails | Idris.Core.Unify |
| fail_fn | Idris.Core.Unify |
| fail_param | Idris.Core.Unify |
| fail_sourceloc | Idris.Core.Unify |
| falseDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| falseTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fancifyAnnots | Idris.Delaborate |
| FAny | IRTS.Lang, IRTS.Defunctionalise |
| FApp | 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 |
| FCon | IRTS.Lang, IRTS.Defunctionalise |
| FConstructor | IRTS.Lang, IRTS.Defunctionalise |
| fc_end | Idris.Core.TT |
| fc_fname | Idris.Core.TT |
| fc_start | Idris.Core.TT |
| FD | Idris.Docs |
| FDesc | IRTS.Lang, IRTS.Defunctionalise |
| FFI | IRTS.JavaScript.AST |
| ffi | IRTS.JavaScript.AST |
| FFIArg | IRTS.JavaScript.AST |
| FFICode | IRTS.JavaScript.AST |
| FFIError | IRTS.JavaScript.AST |
| FFunction | IRTS.Lang, IRTS.Defunctionalise |
| FFunctionIO | IRTS.Lang, IRTS.Defunctionalise |
| fget | Idris.ASTUtils |
| fgetState | Idris.ASTUtils |
| Field | |
| 1 (Type/Class) | Idris.ASTUtils |
| 2 (Data Constructor) | Idris.ASTUtils |
| 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 |
| findExports | IRTS.Exports |
| findFC | Idris.Parser |
| findImport | Idris.Imports |
| findInPath | Idris.Imports |
| findInstances | Idris.ElabTerm |
| findPkgIndex | Idris.Imports |
| findStatics | Idris.AbsSyntax |
| findUnique | Idris.Elab.Clause |
| findUsedArgs | Idris.Core.CaseTree |
| FIO | IRTS.Lang, IRTS.Defunctionalise |
| Fix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixColour | Idris.Parser |
| 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 |
| float | Idris.ParseHelpers, Idris.Parser |
| FManagedPtr | IRTS.Lang, IRTS.Defunctionalise |
| fmapMB | Idris.Core.TT |
| fmodify | Idris.ASTUtils |
| fmodifyState | Idris.ASTUtils |
| FnCase | Idris.Core.CaseTree |
| fnDecl | Idris.Parser |
| fnDecl' | Idris.Parser |
| FnInfo | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fnName | Idris.ParseOps, Idris.Parser |
| FnOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| FnOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fnOpts | Idris.Parser |
| fn_params | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| forall_constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| forall_imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| forCodegen | Idris.AbsSyntax |
| FOREIGNCALL | IRTS.Bytecode |
| ForeignFun | Util.DynamicLinker |
| forget | Idris.Core.TT |
| forgetEnv | Idris.Core.TT |
| Forgot | Idris.Core.TT |
| FPtr | IRTS.Lang, IRTS.Defunctionalise |
| fputState | Idris.ASTUtils |
| freeNames | Idris.Core.TT |
| fromTTMaybe | Idris.ElabTerm |
| Frozen | Idris.Core.Evaluate |
| fset | Idris.ASTUtils |
| FStatic | IRTS.Lang, IRTS.Defunctionalise |
| FStr | IRTS.Lang, IRTS.Defunctionalise |
| FString | IRTS.Lang, IRTS.Defunctionalise |
| FType | IRTS.Lang, IRTS.Defunctionalise |
| Full | Idris.IdeMode |
| FullDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fullExpr | Idris.ParseExpr, Idris.Parser |
| fullTactic | Idris.ParseExpr, Idris.Parser |
| Fun | Util.DynamicLinker |
| Function | Idris.Core.Evaluate |
| FunctionColour | Idris.Colours |
| functionColour | Idris.Colours |
| FunDoc | |
| 1 (Data Constructor) | Idris.Docs |
| 2 (Type/Class) | Idris.Docs |
| FunDoc' | Idris.Docs |
| FUnit | IRTS.Lang, IRTS.Defunctionalise |
| FUnknown | IRTS.Lang, IRTS.Defunctionalise |
| FunOutput | Idris.Core.TT |
| fun_handle | Util.DynamicLinker |
| fun_name | Util.DynamicLinker |
| GD | Idris.Core.ProofTerm, Idris.Core.ProofState, Idris.Core.Elaborate |
| genAll | Idris.Coverage |
| genArgs | IRTS.Defunctionalise |
| genClauses | Idris.Coverage |
| generate | IRTS.Compiler |
| generateDocs | Idris.IdrisDoc |
| getAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getAllNames | Idris.AbsSyntax |
| getArgTys | Idris.Core.TT |
| getAutoImports | Idris.AbsSyntax |
| getAux | Idris.Core.Elaborate |
| getBC | Idris.REPL |
| getCC | IRTS.System |
| getClause | Idris.CaseSplit |
| getClient | Idris.REPL |
| getCmdLine | Idris.AbsSyntax |
| getCodegen | Idris.REPL |
| getCoercionsTo | Idris.AbsSyntax |
| getColour | Idris.REPL |
| getConsoleWidth | Idris.REPL |
| getConsts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getContext | Idris.AbsSyntax |
| getCPU | Idris.REPL |
| getDataDir | IRTS.System |
| getDataFileName | IRTS.System |
| getDocs | Idris.Docs |
| getDumpCases | Idris.AbsSyntax |
| getDumpDefun | Idris.AbsSyntax |
| getErasureInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getErasureUsage | Idris.AbsSyntax |
| getErrSpan | Idris.Error |
| getEvalExpr | Idris.REPL |
| getExecScript | Idris.REPL |
| getExecutablePom | IRTS.System |
| getExpNames | IRTS.Exports |
| getExports | Idris.AbsSyntax |
| getExps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getFC | Idris.ParseHelpers, Idris.Parser |
| getFile | Idris.REPL |
| getFixedInType | Idris.Elab.Utils |
| getFlags | Idris.AbsSyntax |
| getFlexInType | Idris.Elab.Utils |
| getFn | IRTS.Defunctionalise |
| getFunctionErrorHandlers | Idris.AbsSyntax |
| getHdrs | Idris.AbsSyntax |
| getIBCSubDir | Idris.REPL |
| getIdrisLibDir | IRTS.System |
| getIdrisUserDataDir | Idris.REPL |
| GetIdrisVersion | Idris.IdeMode |
| getImportDir | Idris.REPL |
| getImported | Idris.AbsSyntax |
| 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 |
| getLen | Idris.IdeMode |
| 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 |
| getNChar | Idris.IdeMode |
| getNextName | IRTS.Lang, IRTS.Defunctionalise |
| getNoBanner | Idris.AbsSyntax |
| getObjectFiles | Idris.AbsSyntax |
| getOptimisation | Idris.REPL |
| getOptimise | Idris.AbsSyntax |
| getOptLevel | Idris.REPL |
| GetOpts | Idris.IdeMode |
| getOutput | Idris.REPL |
| getOutputTy | Idris.REPL |
| getParamsInType | Idris.Elab.Utils |
| getPArity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getPBtys | Idris.Elab.Utils |
| getPkg | Idris.REPL |
| getPkgCheck | Idris.REPL |
| getPkgClean | Idris.REPL |
| getPkgDir | Idris.REPL |
| getPkgIndex | Idris.REPL |
| getPkgMkDoc | Idris.REPL |
| getPkgREPL | Idris.REPL |
| getPkgTest | Idris.REPL |
| getPort | Idris.REPL |
| getPriority | Idris.AbsSyntax |
| getProofClause | Idris.CaseSplit |
| getProofTerm | Idris.Core.ProofTerm |
| getProvenance | Idris.Core.ProofState, Idris.Core.Elaborate |
| getProvided | Idris.Providers |
| getQuiet | Idris.AbsSyntax |
| getRetTy | Idris.Core.TT |
| getScreenWidth | Util.ScreenSize |
| getScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getShowArgs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getSO | Idris.AbsSyntax |
| getSpecApps | Idris.PartialEval |
| getStaticNames | Idris.Elab.Utils |
| getStatics | Idris.Elab.Utils |
| getSymbol | Idris.AbsSyntax |
| getTargetDir | IRTS.System |
| getTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getTotality | Idris.AbsSyntax |
| getTriple | Idris.REPL |
| getUnboundImplicits | Idris.AbsSyntax |
| getUndefined | Idris.AbsSyntax |
| getUnifyLog | Idris.Core.Elaborate |
| getUniq | Idris.CaseSplit |
| getUniqueUsed | Idris.Elab.Utils |
| getUnmatchable | Idris.ElabTerm |
| getWidth | Idris.AbsSyntax |
| get_autos | Idris.Core.Elaborate |
| get_context | Idris.Core.Elaborate |
| get_deferred | Idris.Core.Elaborate |
| get_dotterm | Idris.Core.Elaborate |
| get_env | Idris.Core.Elaborate |
| get_guess | Idris.Core.Elaborate |
| get_holes | Idris.Core.Elaborate |
| get_inj | Idris.Core.Elaborate |
| get_instances | Idris.Core.Elaborate |
| get_probs | Idris.Core.Elaborate |
| get_recents | Idris.Core.Elaborate |
| get_term | Idris.Core.Elaborate |
| get_type | Idris.Core.Elaborate |
| get_type_val | Idris.Core.Elaborate |
| GHole | Idris.Core.TT |
| GivenVal | Idris.Core.TT |
| Glob | IRTS.Lang, IRTS.Defunctionalise |
| Goal | Idris.Core.ProofTerm, Idris.Core.ProofState, Idris.Core.Elaborate |
| goal | |
| 1 (Function) | Idris.Core.ProofTerm |
| 2 (Function) | Idris.Core.Elaborate |
| goalAtFocus | Idris.Core.ProofState, Idris.Core.Elaborate |
| GoalType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| goalType | Idris.Core.ProofTerm, Idris.Core.ProofState, Idris.Core.Elaborate |
| goal_polymorphic | Idris.ElabTerm |
| groupsOf | IRTS.Defunctionalise |
| gteProp | Idris.ParseHelpers, Idris.Parser |
| gtProp | Idris.ParseHelpers, Idris.Parser |
| Guarded | Idris.Coverage |
| Guardedness | Idris.Coverage |
| Guess | Idris.Core.TT |
| handleError | Idris.Core.Elaborate |
| Header | Idris.Docstrings |
| Help | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| help | Idris.REPLParser |
| helphead | Idris.REPL |
| Hidden | Idris.Core.Evaluate |
| HideDisplay | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| hide_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| highestFC | 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 | |
| 1 (Data Constructor) | Idris.Core.TT |
| 2 (Type/Class) | Idris.Core.ProofTerm |
| holes | Idris.Core.ProofState, Idris.Core.Elaborate |
| HowMuchDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| HRule | Idris.Docstrings |
| hsimpleExpr | Idris.ParseExpr, Idris.Parser |
| HtmlBlock | Idris.Docstrings |
| HTMLOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| I | Idris.Core.TT |
| 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 |
| IBCExport | 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 |
| IBCFnInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCFunctionErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCHeader | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCImportDir | 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 |
| IBCMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCModDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCNameHint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCObj | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCParsedRegion | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ibcPath | Idris.Imports |
| ibcPathNoFallback | Idris.Imports |
| ibcPathWithFallback | Idris.Imports |
| IBCPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCStatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCSubDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTotCheckErr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCTrans | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCUsage | 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_exports | Idris.IBC |
| ibc_fixes | Idris.IBC |
| ibc_flags | Idris.IBC |
| ibc_fninfo | Idris.IBC |
| ibc_function_errorhandlers | Idris.IBC |
| ibc_hdrs | Idris.IBC |
| ibc_implicits | Idris.IBC |
| ibc_importdirs | 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_metavars | Idris.IBC |
| ibc_moduledocs | Idris.IBC |
| ibc_namehints | Idris.IBC |
| ibc_objs | Idris.IBC |
| ibc_optimise | Idris.IBC |
| ibc_parsedSpan | Idris.IBC |
| ibc_patdefs | Idris.IBC |
| ibc_postulates | Idris.IBC |
| ibc_statics | Idris.IBC |
| ibc_syntax | Idris.IBC |
| ibc_total | Idris.IBC |
| ibc_totcheckfail | Idris.IBC |
| ibc_transforms | Idris.IBC |
| ibc_usage | Idris.IBC |
| ibc_write | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdeMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Idemode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idemode | Idris.REPL |
| IdeModeCommand | Idris.IdeMode |
| ideModeEpoch | Idris.IdeMode |
| ideModeForceTermImplicits | Idris.REPL |
| idemodeProcess | Idris.REPL |
| idemodePutSExp | Idris.Output |
| ideModeReturnAnnotated | Idris.Output |
| ideModeReturnWithStatus | Idris.Output |
| IdemodeSocket | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idemodeStart | Idris.REPL |
| identifier | Idris.ParseHelpers, Idris.Parser |
| iderr | Idris.Elab.Utils |
| idiom | Idris.ParseExpr, Idris.Parser |
| IDR | Idris.Imports |
| Idris | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris | Idris.REPL |
| idrisCatch | Idris.Error |
| 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 |
| IdrisParser | Idris.ParseHelpers, Idris.Parser |
| idrisStyle | Idris.ParseHelpers, Idris.Parser |
| idris_calledgraph | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_callgraph | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_callswho | 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_erasureUsed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_errRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_exports | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_fixities | Idris.ASTUtils |
| idris_flags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_fninfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_function_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_hdrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_implicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_imported | 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_moduledocs | 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_outputmode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_parsedSpan | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_patdefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_postulates | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_repl_defs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_scprims | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_statics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_symbols | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_totcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_totcheckfail | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_transforms | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_tyinfodata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_whocalls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ierror | Idris.Error |
| ifail | Idris.Error |
| IFileType | Idris.Imports |
| iLOG | Idris.AbsSyntax |
| Image | Idris.Docstrings |
| Imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Impl | Idris.Core.TT |
| 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 |
| ImplicitInfo | Idris.Core.TT |
| implicitise | Idris.AbsSyntax |
| implicitNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ImplicitS | Idris.PartialEval |
| ImportDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| importDirs | IRTS.CodegenCommon |
| imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| import_ | Idris.Parser |
| Impossible | Idris.Core.TT |
| ImpossibleCase | Idris.Core.CaseTree |
| impShow | Idris.AbsSyntax |
| imp_methods | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Inaccessible | Idris.Core.TT |
| inaccessible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InaccessibleArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| inaccessibleArgs | Idris.Elab.Utils |
| inaccessibleImps | Idris.Elab.Utils |
| iName | Idris.ParseHelpers, Idris.Parser |
| inblock | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| includes | IRTS.CodegenCommon |
| 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.Elab.Utils |
| InferredVal | Idris.Core.TT |
| 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 |
| infP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| infTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initContext | Idris.Core.Evaluate |
| initDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initElabCtxt | Idris.ElabTerm |
| initElaborator | Idris.Core.Elaborate |
| initEState | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initEval | Idris.Core.Evaluate |
| initIBC | Idris.IBC |
| initIdemodeSocket | Idris.REPL |
| 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 | |
| 1 (Data Constructor) | IRTS.Lang, IRTS.Defunctionalise |
| 2 (Type/Class) | Idris.Docstrings |
| inline | IRTS.Inliner |
| inlineAll | IRTS.LangOpts |
| inlineDef | Idris.Inliner |
| inlineTerm | Idris.Inliner |
| inPattern | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| insertScript | Idris.REPL |
| installedPackages | Idris.Imports |
| installIBC | Pkg.Package |
| installIdx | Pkg.Package |
| installObj | Pkg.Package |
| installPkg | Pkg.Package |
| Instance | Idris.Core.ProofState, Idris.Core.Elaborate |
| instanceArg | Idris.Core.Elaborate |
| instanceBlock | Idris.Parser |
| InstanceCtorN | Idris.Core.TT |
| 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.IdeMode |
| integerReader | Idris.CmdOptions |
| Interface | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| interfaces | IRTS.CodegenCommon |
| interMap | IRTS.DumpBC |
| internalExpr | Idris.ParseExpr, Idris.Parser |
| InternalMsg | Idris.Core.TT |
| Interpret | Idris.IdeMode |
| 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 |
| intTyWidth | Idris.Core.TT |
| invalidOperators | Idris.ParseHelpers, Idris.Parser |
| InvalidTCArg | Idris.Core.TT |
| IOption | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| iPrintError | Idris.Output |
| iPrintFunTypes | Idris.Output |
| iPrintResult | Idris.Output |
| iPrintTermWithType | Idris.Output |
| iPrintWithStatus | Idris.Output |
| iputGoal | Idris.Output |
| iputStrLn | Idris.Output |
| iRender | Idris.Output |
| iRenderError | Idris.Output |
| iRenderOutput | Idris.Output |
| iRenderResult | Idris.Output |
| isConName | Idris.Core.Evaluate |
| isConst | IRTS.Bytecode |
| isDConName | Idris.Core.Evaluate |
| isEol | Idris.ParseHelpers, Idris.Parser |
| isetLoadedRegion | Idris.AbsSyntax |
| isetPrompt | Idris.AbsSyntax |
| isFnName | Idris.Core.Evaluate |
| isHole | Idris.Core.Typecheck |
| isHoleName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isInjective | Idris.Core.TT |
| isMetavarName | Idris.AbsSyntax |
| isPostulateName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IState | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isTCDict | Idris.Core.Evaluate |
| isTConName | Idris.Core.Evaluate |
| IsTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isTyInferred | Idris.AbsSyntax |
| IsType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| isType | Idris.Core.Typecheck |
| isTypeConst | Idris.Core.TT |
| ist_callgraph | Idris.ASTUtils |
| ist_optimisation | Idris.ASTUtils |
| isUndefined | Idris.AbsSyntax |
| isUniverse | Idris.Core.Evaluate |
| isWindows | Util.System |
| is_guess | Idris.Core.Elaborate |
| is_scoped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IT16 | Idris.Core.TT |
| IT32 | Idris.Core.TT |
| IT64 | Idris.Core.TT |
| IT8 | Idris.Core.TT |
| italic | Idris.Colours |
| ItalicText | Idris.Core.TT |
| 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.Output |
| JavaScript | IRTS.CodegenJavaScript |
| JS | IRTS.JavaScript.AST |
| JSAlloc | IRTS.JavaScript.AST |
| jsAnd | IRTS.JavaScript.AST |
| JSAnnotation | |
| 1 (Data Constructor) | IRTS.JavaScript.AST |
| 2 (Type/Class) | IRTS.JavaScript.AST |
| JSApp | IRTS.JavaScript.AST |
| JSArray | IRTS.JavaScript.AST |
| JSAssign | IRTS.JavaScript.AST |
| JSBigInt | IRTS.JavaScript.AST |
| jsBigInt | IRTS.JavaScript.AST |
| JSBigIntExpr | IRTS.JavaScript.AST |
| JSBigOne | IRTS.JavaScript.AST |
| JSBigZero | IRTS.JavaScript.AST |
| JSBinOp | IRTS.JavaScript.AST |
| jsCall | IRTS.JavaScript.AST |
| JSCharTy | IRTS.JavaScript.AST |
| JSCond | IRTS.JavaScript.AST |
| JSConstructor | IRTS.JavaScript.AST |
| jsEq | IRTS.JavaScript.AST |
| JSError | IRTS.JavaScript.AST |
| JSFalse | IRTS.JavaScript.AST |
| JSFFI | IRTS.JavaScript.AST |
| JSFloat | IRTS.JavaScript.AST |
| JSFloatTy | IRTS.JavaScript.AST |
| JSForgotTy | IRTS.JavaScript.AST |
| JSFunction | IRTS.JavaScript.AST |
| JSIdent | IRTS.JavaScript.AST |
| JSIndex | IRTS.JavaScript.AST |
| jsInstanceOf | IRTS.JavaScript.AST |
| JSInt | IRTS.JavaScript.AST |
| JSInteger | |
| 1 (Data Constructor) | IRTS.JavaScript.AST |
| 2 (Type/Class) | IRTS.JavaScript.AST |
| JSIntegerTy | IRTS.JavaScript.AST |
| JSIntTy | IRTS.JavaScript.AST |
| jsIsNull | IRTS.JavaScript.AST |
| jsIsNumber | IRTS.JavaScript.AST |
| jsMeth | IRTS.JavaScript.AST |
| JSNew | IRTS.JavaScript.AST |
| JSNoop | IRTS.JavaScript.AST |
| jsNotEq | IRTS.JavaScript.AST |
| JSNull | IRTS.JavaScript.AST |
| JSNum | |
| 1 (Data Constructor) | IRTS.JavaScript.AST |
| 2 (Type/Class) | IRTS.JavaScript.AST |
| jsOr | IRTS.JavaScript.AST |
| jsPackSBits16 | IRTS.JavaScript.AST |
| jsPackSBits32 | IRTS.JavaScript.AST |
| jsPackSBits8 | IRTS.JavaScript.AST |
| jsPackUBits16 | IRTS.JavaScript.AST |
| jsPackUBits32 | IRTS.JavaScript.AST |
| jsPackUBits8 | IRTS.JavaScript.AST |
| JSParens | IRTS.JavaScript.AST |
| JSPostOp | IRTS.JavaScript.AST |
| JSPreOp | IRTS.JavaScript.AST |
| JSProj | IRTS.JavaScript.AST |
| JSPtrTy | IRTS.JavaScript.AST |
| JSRaw | IRTS.JavaScript.AST |
| JSReturn | IRTS.JavaScript.AST |
| JSSeq | IRTS.JavaScript.AST |
| JSString | IRTS.JavaScript.AST |
| JSStringTy | IRTS.JavaScript.AST |
| JSSwitch | IRTS.JavaScript.AST |
| JSTarget | IRTS.CodegenJavaScript |
| JSTernary | IRTS.JavaScript.AST |
| JSThis | IRTS.JavaScript.AST |
| JSTrue | IRTS.JavaScript.AST |
| JSType | |
| 1 (Data Constructor) | IRTS.JavaScript.AST |
| 2 (Type/Class) | IRTS.JavaScript.AST |
| jsTypeOf | IRTS.JavaScript.AST |
| JSUndefined | IRTS.JavaScript.AST |
| jsUnPackBits | IRTS.JavaScript.AST |
| JSWhile | IRTS.JavaScript.AST |
| JSWord | |
| 1 (Data Constructor) | IRTS.JavaScript.AST |
| 2 (Type/Class) | IRTS.JavaScript.AST |
| JSWord16 | IRTS.JavaScript.AST |
| JSWord32 | IRTS.JavaScript.AST |
| JSWord64 | IRTS.JavaScript.AST |
| JSWord8 | IRTS.JavaScript.AST |
| keepGiven | Idris.Core.ProofState, Idris.Core.Elaborate |
| keepTerminator | Idris.ParseHelpers, Idris.Parser |
| Keyword | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| KeywordColour | Idris.Colours |
| keywordColour | Idris.Colours |
| known_classes | Idris.ASTUtils |
| known_terms | Idris.ASTUtils |
| L | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | IRTS.Bytecode |
| LAllocate | IRTS.Lang, IRTS.Defunctionalise |
| LAlt | 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 |
| 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 |
| lastTokenSpan | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LaTeXOutput | 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 |
| LE | IRTS.Lang, IRTS.Defunctionalise |
| LeftErr | Idris.AbsSyntax |
| LendOnly | Idris.Core.Typecheck |
| 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 |
| let_binding | 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 |
| LFNegate | 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 |
| liftDecls | IRTS.CodegenCommon |
| lifte | Idris.Prover |
| liftname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| liftPats | Idris.Core.TT |
| LiftState | IRTS.Lang, IRTS.Defunctionalise |
| LineBreak | Idris.Docstrings |
| lineNum | Idris.ParseHelpers, Idris.Parser |
| Link | Idris.Docstrings |
| LIntCh | IRTS.Lang, IRTS.Defunctionalise |
| LIntFloat | IRTS.Lang, IRTS.Defunctionalise |
| LIntStr | IRTS.Lang, IRTS.Defunctionalise |
| List | Idris.Docstrings |
| 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.IdeMode |
| loadFromIFile | Idris.Parser |
| loadIBC | Idris.IBC |
| LoadingFailed | Idris.Core.TT |
| loadInputs | Idris.REPL |
| loadModule | Idris.Parser |
| loadModule' | Idris.Parser |
| loadPkgIndex | Idris.IBC |
| loadSource | Idris.Parser |
| loadSource' | Idris.Parser |
| loadState | Idris.Core.Elaborate |
| Loc | IRTS.Lang, IRTS.Defunctionalise |
| logLevel | Idris.AbsSyntax |
| LogLvl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| logLvl | Idris.AbsSyntax |
| 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 |
| lookupDefAccExact | Idris.Core.Evaluate |
| lookupDefExact | Idris.Core.Evaluate |
| lookupMetaInformation | Idris.Core.Evaluate |
| lookupNameDef | Idris.Core.Evaluate |
| lookupNames | Idris.Core.Evaluate |
| lookupNameTotal | Idris.Core.Evaluate |
| lookupP | Idris.Core.Evaluate |
| lookupP_all | Idris.Core.Evaluate |
| lookupTotal | Idris.Core.Evaluate |
| lookupTy | Idris.Core.Evaluate |
| lookupTyEnv | Idris.Core.Evaluate |
| lookupTyExact | Idris.Core.Evaluate |
| lookupTyName | Idris.Core.Evaluate |
| lookupTyNameExact | 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 |
| LProj | IRTS.Lang, IRTS.Defunctionalise |
| LReadFile | IRTS.Lang, IRTS.Defunctionalise |
| LReadStr | IRTS.Lang, IRTS.Defunctionalise |
| LRegisterPtr | 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 |
| LSystemInfo | 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 |
| LVMPtr | IRTS.Lang, IRTS.Defunctionalise |
| LWriteFile | IRTS.Lang, IRTS.Defunctionalise |
| LWriteStr | IRTS.Lang, IRTS.Defunctionalise |
| LXOr | IRTS.Lang, IRTS.Defunctionalise |
| LZExt | IRTS.Lang, IRTS.Defunctionalise |
| machine_inf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| make | Pkg.Package |
| MakeDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MakeLemma | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| makeLemma | Idris.Interactive |
| MakeWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| makeWith | Idris.Interactive |
| MakeWithBlock | Idris.IdeMode |
| ManagedPtrType | Idris.Core.TT |
| Many | Idris.Core.Typecheck |
| ManyArgs | Idris.Help |
| mapCtxt | Idris.Core.TT |
| mapDefCtxt | Idris.Core.Evaluate |
| mapPT | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapsnd | Idris.AbsSyntax |
| Match | Idris.Core.Unify |
| 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 |
| MavenProject | IRTS.CodegenCommon |
| maxline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| maybeWithNS | Idris.ParseHelpers, Idris.Parser |
| maybe_default | Idris.ASTUtils |
| MetaInformation | Idris.Core.Evaluate |
| MetaVarArg | Idris.Help |
| Metavariables | Idris.IdeMode |
| MetavarOutput | Idris.Core.TT |
| Metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MethodN | Idris.Core.TT |
| Missing | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mkApp | Idris.Core.TT |
| mkApply | IRTS.Defunctionalise |
| mkApplyCase | IRTS.Defunctionalise |
| mkBigCase | IRTS.Defunctionalise |
| MKCON | IRTS.Bytecode |
| mkDirCmd | Pkg.Package |
| mkEval | IRTS.Defunctionalise |
| mkFieldName | Idris.Erasure |
| mkFnCon | IRTS.Defunctionalise |
| mkForce | Idris.Core.CaseTree |
| mkIBC | Idris.IBC |
| mkList | Idris.ElabTerm |
| 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 |
| mkProofTerm | Idris.Core.ProofTerm |
| mkStatic | Idris.Elab.Utils |
| mkStaticTy | Idris.Elab.Utils |
| mkTTName | Idris.DSL |
| mkType | Idris.ParseExpr, Idris.Parser |
| mkUnderCon | IRTS.Defunctionalise |
| mkUniqueNames | Idris.AbsSyntax |
| mkWith | Idris.CaseSplit |
| MN | Idris.Core.TT |
| ModDoc | Idris.Docs |
| modDocName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| mutual_types | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mut_nesting | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Name | Idris.Core.TT |
| name | Idris.ParseHelpers, Idris.Parser |
| NameArg | Idris.Help |
| NamedInstanceDoc | Idris.Docs |
| nameMissing | Idris.CaseSplit |
| NameOutput | Idris.Core.TT |
| NamePart | Idris.Core.TT |
| nameRoot | Idris.CaseSplit |
| namesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| namespace | |
| 1 (Function) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Function) | Idris.Parser |
| NamespaceArg | Idris.Help |
| namesUsed | Idris.Core.CaseTree |
| NameTArg | Idris.ParseExpr, Idris.Parser |
| NameType | Idris.Core.TT |
| Native | IRTS.Lang, IRTS.Defunctionalise |
| NativeTy | Idris.Core.TT |
| nativeTyWidth | Idris.Core.TT |
| natural | Idris.ParseHelpers, Idris.Parser |
| NErased | Idris.Core.TT |
| Never | Idris.Core.Typecheck |
| NewDefn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| newProof | Idris.Core.ProofState, Idris.Core.Elaborate |
| new_tyDecls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| nextN | IRTS.LangOpts |
| 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 |
| noDocCommentHere | Idris.ParseHelpers, Idris.Parser |
| noDocs | Idris.Docstrings |
| NoEliminator | Idris.Core.TT |
| noErrors | Idris.AbsSyntax |
| nofixityoperator | Idris.ParseOps, Idris.Parser |
| NoImplicit | Idris.AbsSyntaxTree, 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) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | IRTS.BCImp |
| 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 |
| nowElaboratingPS | Idris.Core.ProofState, Idris.Core.Elaborate |
| now_elaborating | Idris.Core.Elaborate |
| 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 |
| nt_unique | Idris.Core.TT |
| NULL | IRTS.Bytecode |
| nullDocstring | Idris.Docstrings |
| NullType | Idris.Core.TT |
| NumberArg | Idris.Help |
| Object | IRTS.CodegenCommon |
| occurrences | Idris.Core.TT |
| OK | Idris.Core.TT |
| OLogging | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Once | Idris.Core.Typecheck |
| 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 |
| opExpr | Idris.ParseExpr, Idris.Parser |
| Opt | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Type/Class) | Idris.IdeMode |
| opt | Idris.REPL |
| Optimisable | Idris.DataOpts |
| Optimisation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Optimise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OptInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Option | Idris.Core.TT |
| OptionalArg | Idris.Help |
| OptionArg | Idris.Help |
| OptLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opts_idrisCmdline | Idris.ASTUtils |
| opt_autoImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_autoSolve | Idris.AbsSyntaxTree, 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_detaggable | Idris.ASTUtils |
| opt_errContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_ibcsubdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_importdirs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_inaccessible | Idris.ASTUtils |
| opt_logLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_nobanner | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_optimise | 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 |
| outputFile | IRTS.CodegenCommon |
| OutputFmt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OutputMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OutputTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| outputTy | Idris.AbsSyntax |
| OutputType | IRTS.CodegenCommon |
| outputType | IRTS.CodegenCommon |
| overload | Idris.ParseData, Idris.Parser |
| Overview | Idris.IdeMode |
| overview | Idris.Docstrings |
| OverviewDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| P | Idris.Core.TT |
| pAccess | Idris.IBC |
| pairCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pairTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAlternative | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAppBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAppImpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Para | Idris.Docstrings |
| paramNames | Idris.Elab.Utils |
| params | |
| 1 (Function) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Function) | Idris.Parser |
| param_pos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ParentN | Idris.Core.TT |
| PArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PArg' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pargopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parseCmd | Idris.REPLParser |
| parseCodegen | Idris.CmdOptions |
| parseConsoleWidth | Idris.CmdOptions |
| parseConst | Idris.Parser |
| parseDocstring | Idris.Docstrings |
| parseExpr | Idris.Parser |
| parseFlags | Idris.CmdOptions |
| parseImports | Idris.Parser |
| parseMessage | Idris.IdeMode |
| parseProg | Idris.Parser |
| parser | Idris.CmdOptions |
| parserWarnings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parseTactic | Idris.Parser |
| parseVersion | Idris.CmdOptions |
| Partial | Idris.Core.Evaluate |
| PartialFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| partial_eval | Idris.PartialEval |
| PAs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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.Elab.Utils |
| pbty | Idris.Elab.Utils |
| 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 |
| 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 |
| performUsageAnalysis | Idris.Erasure |
| pErrorHandlers | Idris.IBC |
| pErrRev | Idris.IBC |
| PETransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pexp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pExports | Idris.IBC |
| pe_app | Idris.PartialEval |
| pe_clauses | Idris.PartialEval |
| pe_def | Idris.PartialEval |
| pe_simple | Idris.PartialEval |
| PFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pFixes | Idris.IBC |
| pFlags | Idris.IBC |
| pFnInfo | 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 |
| pImportDirs | Idris.IBC |
| pImports | Idris.IBC |
| PImpossible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pImps | Idris.IBC |
| PInferRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pInstances | Idris.IBC |
| piOpts | Idris.ParseExpr, Idris.Parser |
| pKeywords | Idris.IBC |
| Pkg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgArgs | Idris.Help |
| PkgBuild | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgClean | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgIndex | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pkgIndex | Idris.Imports |
| PkgInstall | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgMkDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgTest | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Placeholder | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PLam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLangExt | Idris.Parser |
| PLaterdecl | 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 |
| pMDocs | Idris.IBC |
| pMetaInformation | Idris.IBC |
| PMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pMetavars | Idris.IBC |
| 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 |
| popIndent | Idris.ParseHelpers, Idris.Parser |
| pOptimise | Idris.IBC |
| pop_estack | Idris.AbsSyntax |
| Port | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| postulate | Idris.Parser |
| PostulateColour | Idris.Colours |
| postulateColour | Idris.Colours |
| PostulateOutput | Idris.Core.TT |
| PPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pparam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PParams | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pParsedSpan | Idris.IBC |
| pPatdefs | Idris.IBC |
| PPatvar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPOption | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ppOption | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ppOptionIst | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ppopt_impl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pPostulates | Idris.IBC |
| PPrint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pprintConstDocs | Idris.Docs |
| pprintDef | Idris.REPL |
| pprintDelab | Idris.Delaborate |
| pprintDelabTy | Idris.Delaborate |
| pprintDocs | Idris.Docs |
| pprintErr | Idris.Delaborate |
| pprintPTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pprintTT | Idris.Core.TT |
| PProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProvider | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuasiquote | 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 |
| PrefixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRefl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prel | Idris.DataOpts |
| premises | Idris.Core.ProofTerm, Idris.Core.ProofState, Idris.Core.Elaborate |
| prepare_apply | Idris.Core.Elaborate |
| PrepFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| preProcOpts | Idris.CmdOptions |
| prep_fill | Idris.Core.Elaborate |
| PResolveTC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prettyDocumentedIst | Idris.Output |
| prettyEnv | Idris.Core.TT |
| prettyImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prettyIst | 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 |
| primitives | Idris.Primitives |
| primNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PrintDef | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| printUndefinedNames | Idris.Output |
| 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 |
| processTacticDecls | Idris.ElabTerm |
| 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.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| 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 | |
| 1 (Type/Class) | Idris.Core.ProofTerm |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proof_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| propagateParams | Idris.Elab.Clause |
| Prove | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prove | Idris.Prover |
| Provenance | Idris.Core.TT |
| prover | Idris.Prover |
| proverCompletion | Idris.Completion |
| proverSettings | Idris.Prover |
| Provide | Idris.Providers |
| Provided | Idris.Providers |
| provider | Idris.Parser |
| ProviderError | Idris.Core.TT |
| providerTy | Idris.Providers |
| ProvideWhat | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ProvideWhat' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ProvPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ProvTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pruneAlt | Idris.ElabTerm |
| pruneByType | Idris.ElabTerm |
| prunStateT | Idris.Core.Elaborate |
| PRunTactics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PS | Idris.Core.ProofState, Idris.Core.Elaborate |
| pscoped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pscript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pshow | Idris.Output |
| psolve | Idris.Elab.Utils |
| 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 |
| pTotCheckErr | 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 |
| PUniverse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PUnquote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pureArgParser | Idris.CmdOptions |
| pureTerm | Idris.Core.TT |
| pUsage | Idris.IBC |
| pushIndent | Idris.ParseHelpers, Idris.Parser |
| push_estack | Idris.AbsSyntax |
| putIState | Idris.AbsSyntax |
| PVar | Idris.Core.TT |
| pvars | Idris.Elab.Utils |
| 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 |
| qshow | Idris.Core.Elaborate |
| quasiquote | Idris.ParseExpr, Idris.Parser |
| Quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quote | Idris.Core.Evaluate |
| quote | Idris.Core.Evaluate |
| quoteGoal | Idris.ParseExpr, Idris.Parser |
| RApp | Idris.Core.TT |
| RArg | Idris.Reflection |
| rArgToPArg | Idris.Reflection |
| Raw | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| rawBool | Idris.ElabTerm |
| rawCons | Idris.ElabTerm |
| RawHtml | Idris.Docstrings |
| 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 |
| RConstraint | Idris.Reflection |
| RDeclare | Idris.Reflection |
| REBASE | IRTS.Bytecode |
| receiveInput | Idris.Prover |
| recents | Idris.Core.ProofState, Idris.Core.Elaborate |
| recheck | Idris.Core.Typecheck |
| recheckC | Idris.Elab.Utils |
| recheckC_borrowing | Idris.Elab.Utils |
| recheck_borrowing | Idris.Core.Typecheck |
| recinfo | Idris.ElabDecls |
| record | Idris.ParseData, Idris.Parser |
| recordType | Idris.ParseExpr, Idris.Parser |
| rec_elabDecl | 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 |
| reflectBinderQuote | Idris.ElabTerm |
| reflectBinderQuotePattern | Idris.ElabTerm |
| reflectConstant | Idris.ElabTerm |
| reflectCtxt | Idris.ElabTerm |
| reflectEnv | Idris.ElabTerm |
| reflectErr | Idris.ElabTerm |
| reflectFC | Idris.ElabTerm |
| Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ReflectionError | Idris.Core.TT |
| ReflectionFailed | Idris.Core.TT |
| reflectName | Idris.ElabTerm |
| reflectNameQuotePattern | Idris.ElabTerm |
| reflectNameType | Idris.ElabTerm |
| reflectRaw | Idris.ElabTerm |
| reflectRawQuote | Idris.ElabTerm |
| reflectRawQuotePattern | Idris.ElabTerm |
| reflectTTQuote | Idris.ElabTerm |
| reflectTTQuotePattern | Idris.ElabTerm |
| reflectUExp | Idris.ElabTerm |
| reflectUniverse | Idris.ElabTerm |
| reflErrName | Idris.ElabTerm |
| reflm | Idris.ElabTerm |
| refocus | Idris.Core.ProofTerm |
| refsIn | Idris.Core.TT |
| 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 |
| reifyArithTy | Idris.ElabTerm |
| reifyIntTy | Idris.ElabTerm |
| reifyNativeTy | Idris.ElabTerm |
| reifyRaw | Idris.ElabTerm |
| reifyRawApp | Idris.ElabTerm |
| reifyReportPart | Idris.ElabTerm |
| reifyReportParts | 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 |
| reifyTyDecl | Idris.ElabTerm |
| Reload | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RemoveOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| removeOptimise | Idris.AbsSyntax |
| removeProof | Idris.REPL |
| renderDocstring | Idris.Docstrings |
| renderDocTerm | Idris.Docstrings |
| renderExternal | Idris.Output |
| renderHtml | Idris.Docstrings |
| Reorder | Idris.Core.ProofState, Idris.Core.Elaborate |
| reorder_claims | Idris.Core.Elaborate |
| repl | Idris.REPL |
| replaceSplits | Idris.CaseSplit |
| replCompletion | Idris.Completion |
| REPLCompletions | Idris.IdeMode |
| replPkg | Pkg.Package |
| replSettings | Idris.REPL |
| repl_definitions | Idris.ASTUtils |
| report | Idris.Error |
| reportParserWarnings | Idris.ParseHelpers, Idris.Parser |
| RESERVE | IRTS.Bytecode |
| reserved | Idris.ParseHelpers, Idris.Parser |
| reservedOp | Idris.ParseHelpers, Idris.Parser |
| resetNameIdx | Idris.AbsSyntax |
| resolveProof | Idris.REPL |
| resolveTC | Idris.ElabTerm |
| resTC' | Idris.ElabTerm |
| resultCaseDecls | Idris.ElabTerm |
| resultContext | Idris.ElabTerm |
| resultMetavars | Idris.ElabTerm |
| resultTerm | Idris.ElabTerm |
| resultTyDecls | 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 |
| RExplicit | Idris.Reflection |
| RForce | Idris.Core.TT |
| rhs | Idris.Parser |
| RightOK | Idris.AbsSyntax |
| RImplicit | Idris.Reflection |
| rmFile | Util.System |
| rmIBC | Pkg.Package |
| rmIdx | Pkg.Package |
| RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RTyDecl | Idris.Reflection |
| RType | Idris.Core.TT |
| rt_simplify | Idris.Core.Evaluate |
| Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| runArgParser | Idris.CmdOptions |
| runClient | Idris.REPL |
| runElab | Idris.Core.Elaborate |
| runIdeModeCommand | Idris.REPL |
| runInnerParser | Idris.ParseHelpers, Idris.Parser |
| runIO | Idris.AbsSyntax |
| runMain | Idris.REPL |
| runparser | Idris.ParseHelpers, Idris.Parser |
| runTac | Idris.ElabTerm |
| RunTactic' | Idris.Core.ProofTerm |
| runTactical | Idris.ElabTerm |
| runTactics | Idris.ParseExpr, Idris.Parser |
| RunTime | Idris.Core.CaseTree |
| RUType | Idris.Core.TT |
| RVal | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | IRTS.Bytecode |
| safeForget | Idris.Core.TT |
| safeForgetEnv | Idris.Core.TT |
| safeToEnum | Idris.IBC |
| 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 |
| score | Idris.Core.TT |
| SDecl | IRTS.Simplified |
| SDefaultCase | IRTS.Simplified |
| Search | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| searchByType | Idris.TypeSearch |
| searchPred | Idris.TypeSearch |
| SeqArgs | Idris.Help |
| 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 |
| setAutoSolve | Idris.AbsSyntax |
| 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 |
| setErrSpan | Idris.AbsSyntax |
| setFlags | Idris.AbsSyntax |
| setFnInfo | Idris.AbsSyntax |
| setIBCSubDir | Idris.AbsSyntax |
| setIdeMode | 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 | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| setOptimise | Idris.AbsSyntax |
| setOptLevel | 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) | IRTS.Simplified |
| 2 (Type/Class) | Idris.IdeMode |
| SExpable | Idris.IdeMode |
| SexpList | Idris.IdeMode |
| sexpToCommand | Idris.IdeMode |
| SForeign | IRTS.Simplified |
| SFun | IRTS.Simplified |
| shadow | Idris.AbsSyntax |
| Shared | Idris.Core.CaseTree |
| showCG | Idris.Core.TT |
| showCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDeclImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDecls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showDImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showEnv | Idris.Core.TT |
| showEnv' | Idris.Core.TT |
| showEnvDbg | Idris.Core.TT |
| showErr | Idris.Error |
| ShowImpl | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| 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 |
| ShowPkgs | Idris.AbsSyntaxTree, 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 |
| simpleDecls | IRTS.CodegenCommon |
| SimpleExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| simpleExpr | Idris.ParseExpr, Idris.Parser |
| simpleExternalExpr | Idris.ParseExpr, Idris.Parser |
| 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) | Idris.Core.Elaborate |
| simplifyCasedef | Idris.Core.Evaluate |
| simplifyDefs | IRTS.Simplified |
| singleLineComment | Idris.ParseHelpers, Idris.Parser |
| sInstanceN | Idris.Core.TT |
| SizeChange | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Skip | 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 |
| SNothing | IRTS.Simplified |
| sNS | Idris.Core.TT |
| SoftBreak | Idris.Docstrings |
| Solve | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| solve | Idris.Core.Elaborate |
| solveAll | Idris.ElabTerm |
| solveAuto | Idris.ElabTerm |
| solveAutos | Idris.ElabTerm |
| solved | Idris.Core.ProofState, Idris.Core.Elaborate |
| solveDeferred | Idris.AbsSyntax |
| SOp | IRTS.Simplified |
| SourceFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| sourcefile | Idris.IBC |
| SourceTerm | Idris.Core.TT |
| Space | Idris.Docstrings |
| 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 |
| splitName | Idris.REPL |
| 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 | |
| 1 (Data Constructor) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.Docstrings |
| str | Idris.Core.TT |
| string | Idris.ParseHelpers, Idris.Parser |
| StringAtom | Idris.IdeMode |
| stringLiteral | Idris.ParseHelpers, Idris.Parser |
| StringLitTArg | Idris.ParseExpr, Idris.Parser |
| stripLinear | Idris.AbsSyntax |
| stripUnmatchable | Idris.AbsSyntax |
| Strong | Idris.Docstrings |
| StrType | Idris.Core.TT |
| SubReport | Idris.Core.TT |
| subst | Idris.Core.TT |
| substAlt | Idris.Core.CaseTree |
| substMatch | Idris.AbsSyntax |
| substMatches | Idris.AbsSyntax |
| substMatchesShadow | Idris.AbsSyntax |
| substMatchShadow | Idris.AbsSyntax |
| substNames | Idris.Core.TT |
| substSC | Idris.Core.CaseTree |
| substTerm | Idris.Core.TT |
| substV | Idris.Core.TT |
| SucCase | Idris.Core.CaseTree |
| sUN | Idris.Core.TT |
| SUpdate | IRTS.Simplified |
| SV | IRTS.Simplified |
| Symbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| symbol | Idris.ParseHelpers, Idris.Parser |
| SymbolAtom | Idris.IdeMode |
| 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 |
| syntaxNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntaxRule | Idris.Parser |
| SyntaxRules | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntaxRulesList | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntaxSym | Idris.Parser |
| syntaxSymbols | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntax_keywords | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syntax_rules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SynTm | Idris.ParseExpr, Idris.Parser |
| syn_in_quasiquote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syn_namespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| syn_params | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| T | IRTS.Bytecode |
| table | Idris.ParseOps, Idris.Parser |
| TacImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacimpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacN | Idris.ElabTerm |
| Tactic | Idris.Core.ProofState, Idris.Core.Elaborate |
| tactic | Idris.ParseExpr, Idris.Parser |
| TacticArg | Idris.ParseExpr, Idris.Parser |
| tactics | Idris.ParseExpr, Idris.Parser |
| tacticsExpr | Idris.ParseExpr, Idris.Parser |
| TAILCALL | IRTS.Bytecode |
| TargetCPU | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| targetCPU | |
| 1 (Function) | IRTS.CodegenCommon |
| 2 (Function) | Idris.AbsSyntax |
| TargetTriple | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| targetTriple | |
| 1 (Function) | IRTS.CodegenCommon |
| 2 (Function) | Idris.AbsSyntax |
| TC | Idris.Core.TT |
| TCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TCInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tcinstance | Idris.Core.TT |
| tclift | Idris.Error |
| tcname | Idris.Core.TT |
| TCon | Idris.Core.TT |
| tctry | Idris.Error |
| tc_dictionary | Idris.Core.Evaluate |
| TDocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tempfile | Util.System |
| Term | Idris.Core.TT |
| TermElab | Idris.IdeMode |
| terminator | Idris.ParseHelpers, Idris.Parser |
| TermNoImplicits | Idris.IdeMode |
| TermNormalise | Idris.IdeMode |
| TermPart | Idris.Core.TT |
| TermShowImplicits | Idris.IdeMode |
| TermSize | Idris.Core.TT |
| termsize | Idris.Core.TT |
| TermSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TestInline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| testLib | Pkg.Package |
| testPkg | Pkg.Package |
| TEval | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TextFormatting | Idris.Core.TT |
| TextPart | Idris.Core.TT |
| TFail | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tfail | Idris.Core.TT |
| thead | Idris.Core.TT |
| TheWorld | Idris.Core.TT |
| thname | Idris.Core.ProofState, Idris.Core.Elaborate |
| throwError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TIData | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| timestampOlder | Idris.IBC |
| TIPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TISolution | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| toCons | IRTS.Defunctionalise |
| toConsA | IRTS.Defunctionalise |
| toEither | Idris.AbsSyntax |
| toIBCFile | Pkg.Package |
| TooManyArgs | Idris.Core.TT |
| TooManyArguments | Idris.Core.TT |
| TOPBASE | IRTS.Bytecode |
| Toplevel | Idris.Coverage |
| toplevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| toSExp | Idris.IdeMode |
| 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 |
| traceWhen | Idris.Core.TT |
| transform | Idris.Parser |
| TransformInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| transformPats | Idris.Transforms |
| transformPatsWith | 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 |
| tryCatch | Idris.Core.Elaborate |
| tryFullExpr | Idris.ParseExpr, Idris.Parser |
| tryLoadFn | Util.DynamicLinker |
| tryLoadLib | Util.DynamicLinker |
| tryWhen | Idris.Core.Elaborate |
| TSearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TSeq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TT | Idris.Core.TT |
| 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.IdeMode |
| 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 |
| uconstraint | Idris.Core.TT |
| UCs | Idris.Core.TT |
| UExp | Idris.Core.TT |
| ufc | 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 | |
| 1 (Data Constructor) | Idris.Core.Evaluate |
| 2 (Data Constructor) | Idris.Docstrings |
| Undefine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| underline | Idris.Colours |
| UnderlineText | Idris.Core.TT |
| Undo | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| undo | Idris.Core.Elaborate |
| Unfocus | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Unguarded | Idris.Coverage |
| unIdiom | Idris.DSL |
| unified | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifiedD | Idris.PartialEval |
| Unify | Idris.Core.Unify |
| unify | Idris.Core.Unify |
| UnifyAll | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifyGoal | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyGoal | Idris.Core.Elaborate |
| 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 |
| unify_all | Idris.Core.Elaborate |
| uniqueBinders | Idris.Core.TT |
| uniqueBindersCtxt | Idris.Core.Evaluate |
| UniqueError | Idris.Core.TT |
| UniqueKindError | Idris.Core.TT |
| uniqueName | Idris.Core.TT |
| uniqueNameCtxt | Idris.Core.Evaluate |
| uniqueNameFrom | Idris.Core.TT |
| uniqueNameSet | Idris.Core.TT |
| UniqueType | Idris.Core.TT |
| UniqueUse | Idris.Core.Typecheck |
| unique_hole | Idris.Core.Elaborate |
| unique_hole' | Idris.Core.Elaborate |
| unitCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Universe | Idris.Core.TT |
| 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 |
| unquote | Idris.ParseExpr, Idris.Parser |
| unrecoverable | Idris.Core.Unify |
| UnsetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unwrapFC | Idris.Core.TT |
| upairCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| upairTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| upd | Idris.Coverage |
| Updatable | Idris.Core.CaseTree |
| UPDATE | IRTS.Bytecode |
| updateAux | Idris.Core.Elaborate |
| updateContext | Idris.AbsSyntax |
| updateDef | Idris.Core.TT |
| updateIState | Idris.AbsSyntax |
| updateN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updateNs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updatePS | Idris.Core.Elaborate |
| updateSolved | Idris.Core.ProofTerm |
| updateSolvedTerm | Idris.Core.ProofTerm |
| updateSolvedTerm' | Idris.Core.ProofTerm |
| updateSyntaxRules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| update_term | Idris.Core.Elaborate |
| UsageReason | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UseCodegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UseConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedArg | IRTS.Lang, IRTS.Defunctionalise |
| usedIn | IRTS.Lang, IRTS.Defunctionalise |
| usedNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedns | Idris.Core.ProofState, Idris.Core.Elaborate |
| usedpos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| UType | Idris.Core.TT |
| 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 | |
| 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 |
| verbosePPOption | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| version | IRTS.System |
| Via | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| VImpossible | Idris.Core.Evaluate |
| vinstances | Idris.Core.TT |
| vivid | Idris.Colours |
| VoidType | Idris.Core.TT |
| VP | Idris.Core.Evaluate |
| VProj | Idris.Core.Evaluate |
| VTmp | Idris.Core.Evaluate |
| vToP | Idris.Core.TT |
| VType | Idris.Core.Evaluate |
| VUType | Idris.Core.Evaluate |
| VV | Idris.Core.Evaluate |
| warnDisamb | Idris.Error |
| WarnOnly | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| WarnPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| WarnReach | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| warnTotality | Idris.Output |
| Warranty | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| warranty | Idris.REPL |
| weakenEnv | Idris.Core.TT |
| weakenTm | Idris.Core.TT |
| weakenTmEnv | Idris.Core.TT |
| wExpr | Idris.Parser |
| WhatDocs | Idris.IdeMode |
| whereBlock | Idris.Parser |
| WhereN | Idris.Core.TT |
| while_elaborating | Idris.Core.ProofState, Idris.Core.Elaborate |
| whiteSpace | Idris.ParseHelpers, Idris.Parser |
| WhoCalls | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| whoCalls | Idris.WhoCalls |
| withContext | Idris.AbsSyntax |
| withContext_ | Idris.AbsSyntax |
| withErrorReflection | Idris.ElabTerm |
| WithFnType | Idris.Core.TT |
| WithN | Idris.Core.TT |
| withTempdir | Util.System |
| Wk | Idris.Core.TT |
| WkEnv | Idris.Core.TT |
| WkEnvTT | Idris.Core.TT |
| WorldType | Idris.Core.TT |
| writeIBC | Idris.IBC |
| writePkgIndex | Idris.IBC |
| zipHere | Idris.Core.Elaborate |