Index
| Abandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| accData | Idris.Parser.Helpers, Idris.Parser |
| Accessibility | Idris.Core.Evaluate |
| accessibility | Idris.Parser.Helpers, Idris.Parser |
| accessibility' | Idris.Parser.Helpers, Idris.Parser |
| addAcc | Idris.Parser.Helpers, Idris.Parser |
| addAlist | Idris.Core.TT |
| addApps | IRTS.Defunctionalise |
| addAutoHint | Idris.AbsSyntax |
| addAutoImport | Idris.AbsSyntax |
| addBinder | Idris.Core.TT |
| addCalls | Idris.AbsSyntax |
| 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 |
| addDefinedName | Idris.AbsSyntax |
| addDeprecated | 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 |
| addPSname | Idris.Core.Elaborate |
| addRecord | Idris.AbsSyntax |
| addReplSyntax | Idris.Parser |
| addStatics | Idris.AbsSyntax |
| addSyntax | Idris.Parser |
| addTags | IRTS.Lang, IRTS.Defunctionalise |
| addToCG | Idris.AbsSyntax |
| addToCtxt | Idris.Core.Evaluate |
| ADDTOP | IRTS.Bytecode |
| addToUsing | Idris.AbsSyntax |
| addTrans | Idris.AbsSyntax |
| addTT | 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.REPL.Parser |
| allImportDirs | Idris.AbsSyntax |
| allNames | Idris.AbsSyntax |
| allNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| allNothing | Idris.Coverage |
| allocUnique | IRTS.Lang, IRTS.Defunctionalise |
| allowImp | Idris.Parser.Expr, Idris.Parser |
| allTTNames | Idris.Core.TT |
| AllTypes | Idris.Core.TT |
| AlreadyDefined | Idris.Core.TT |
| alt | Idris.Parser.Expr, Idris.Parser |
| AltsTArg | Idris.Parser.Expr, Idris.Parser |
| AlwaysShow | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| AnnAntiquote | Idris.Core.TT |
| AnnBoundName | Idris.Core.TT |
| AnnConst | Idris.Core.TT |
| AnnData | Idris.Core.TT |
| AnnErr | Idris.Core.TT |
| AnnFC | Idris.Core.TT |
| AnnKeyword | Idris.Core.TT |
| AnnLink | Idris.Core.TT |
| AnnName | Idris.Core.TT |
| annName | Idris.Delaborate |
| AnnNamespace | Idris.Core.TT |
| annotationColour | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| annotCode | Idris.Docstrings |
| AnnQuasiquote | Idris.Core.TT |
| 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.Parser.Expr, Idris.Parser |
| apply | Idris.Core.Elaborate |
| apply' | Idris.Core.Elaborate |
| apply2 | Idris.Core.Elaborate |
| ApplyCase | IRTS.Defunctionalise |
| applyOpts | Idris.DataOpts |
| ApplyTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| applyTransRules | Idris.Transforms |
| applyTransRulesWith | Idris.Transforms |
| apply_elab | Idris.Core.Elaborate |
| AppStatus | Idris.Core.TT |
| 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.Parser.Expr, Idris.Parser |
| argExpr | Idris.Parser |
| argName | Idris.Reflection |
| ArgOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| argPlicity | Idris.Reflection |
| 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 |
| 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 |
| AutoHint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| autoImplicit | Idris.Parser.Expr, Idris.Parser |
| 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 |
| B32 | Idris.Core.TT |
| B64 | Idris.Core.TT |
| B8 | Idris.Core.TT |
| backtick | Idris.Parser.Ops, Idris.Parser |
| basename | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| BE | IRTS.Lang, IRTS.Defunctionalise |
| BelieveMe | Idris.Core.Evaluate |
| BI | Idris.Core.TT |
| bi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Bigger | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| binary | Idris.Parser.Ops, 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.Parser.Helpers, Idris.Parser |
| bindsymbol | Idris.Parser.Expr, Idris.Parser |
| 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.Parser.Expr, Idris.Parser |
| bracketed' | Idris.Parser.Expr, Idris.Parser |
| bracketedExpr | Idris.Parser.Expr, Idris.Parser |
| Browse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| BrowseNS | Idris.IdeMode |
| bugaddr | Idris.Delaborate |
| build | Idris.Elab.Term |
| buildDatatypes | Idris.Reflection |
| buildFunDefns | Idris.Reflection |
| buildMods | Pkg.Package |
| buildPkg | Pkg.Package |
| buildSCG | Idris.Coverage |
| buildSCG' | Idris.Coverage |
| buildTC | Idris.Elab.Term |
| buildTree | Idris.Chaser |
| buildType | Idris.Elab.Type |
| ByReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Bytecode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| caf | Idris.Parser |
| 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.Parser.Expr, 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.Parser.Expr, Idris.Parser |
| 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.Elab.Term |
| 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.Parser.Helpers, Idris.Parser |
| charLiteral | Idris.Parser.Helpers, Idris.Parser |
| Check | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| check | Idris.Core.Typecheck |
| check' | Idris.Core.Typecheck |
| checkAddDef | Idris.Elab.Utils |
| checkAllCovering | Idris.Coverage |
| checkDeclTotality | Idris.Coverage |
| checkDef | Idris.Elab.Utils |
| checkDeprecated | Idris.Elab.Utils |
| checkDocs | Idris.Elab.Utils |
| checkDocstring | Idris.Docstrings |
| checkDSL | Idris.Parser.Data, 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 |
| checkVisibility | Idris.Elab.Utils |
| 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 |
| claimTy | Idris.Reflection |
| 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 |
| clearHighlights | Idris.Output |
| clearIBC | Idris.AbsSyntax |
| clearOrigPats | Idris.AbsSyntax |
| clearParserWarnings | Idris.Parser.Helpers, Idris.Parser |
| clearPTypes | Idris.AbsSyntax |
| clear_totcheck | Idris.AbsSyntax |
| Client | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| closeBlock | Idris.Parser.Helpers, Idris.Parser |
| CmdArg | Idris.Help |
| cmdOptType | Idris.AbsSyntax |
| Codata | Idris.Core.TT |
| codata | Idris.Core.TT |
| Code | Idris.Docstrings |
| CodeBlock | Idris.Docstrings |
| Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegen | Idris.AbsSyntax |
| CodegenArgs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegenC | IRTS.CodegenC |
| codegenCats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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.Parser.Helpers, Idris.Parser |
| collectDeferred | Idris.Elab.Term |
| 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.Parser.Helpers, Idris.Parser |
| Command | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| commaSeparated | Idris.Parser.Helpers, Idris.Parser |
| commentMarkers | Idris.Parser.Helpers, 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 |
| Complete | Idris.Core.TT |
| 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.Parser.Expr, Idris.Parser |
| constants | Idris.Parser.Expr, 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.Parser.Expr, Idris.Parser |
| ConstraintFC | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.Core.TT |
| constraintList | Idris.Parser.Expr, Idris.Parser |
| constraintList1 | Idris.Parser.Expr, Idris.Parser |
| Constructor | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constructor | Idris.Parser.Data, 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.Core.TT |
| 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 |
| DAccess | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DAlt | IRTS.Defunctionalise |
| DApp | IRTS.Defunctionalise |
| Data | Idris.Core.TT |
| DataColour | Idris.Colours |
| dataColour | Idris.Colours |
| DataDoc | Idris.Docs |
| DataErrRev | Idris.Core.TT |
| dataI | Idris.Parser.Data, Idris.Parser |
| DataMI | Idris.Core.Evaluate |
| DataOpt | Idris.Core.TT |
| DataOpts | Idris.Core.TT |
| dataOpts | Idris.Parser.Data, Idris.Parser |
| DataOutput | Idris.Core.TT |
| Datatype | Idris.Core.TT |
| datatypes | Idris.Core.ProofState, Idris.Core.Elaborate |
| data_ | Idris.Parser.Data, Idris.Parser |
| data_opts | Idris.Core.TT |
| DAutoImplicits | 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 |
| DDefault | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DDefaultCase | IRTS.Defunctionalise |
| DDefs | IRTS.Defunctionalise |
| DDeprecate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DDynamicLibs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| declExtension | Idris.Parser |
| declExtensions | Idris.Parser |
| DeclRule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| decorateid | Idris.Elab.Utils |
| decoration | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Def | Idris.Core.Evaluate |
| defaultAlt | IRTS.Bytecode |
| DefaultCase | Idris.Core.CaseTree |
| DefaultCaseFun | Idris.Core.TT |
| DefaultEliminator | Idris.Core.TT |
| defaultImplicit | Idris.Parser.Expr, Idris.Parser |
| defaultOptimise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| defaultOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DefaultPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| delabSugared | Idris.Delaborate |
| delabTy | Idris.Delaborate |
| delabTy' | Idris.Delaborate |
| delayed_elab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| delazy | Idris.Coverage |
| delazy' | Idris.Coverage |
| deleteDefExact | Idris.Core.TT |
| dep_app | Idris.Core.Elaborate |
| DError | IRTS.Defunctionalise |
| DErrorHandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| desugar | Idris.DSL |
| desugarAs | Idris.Elab.AsPat |
| DesugarNats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| detaggable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DExp | IRTS.Defunctionalise |
| DFlag | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DForeign | IRTS.Defunctionalise |
| DFreeze | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DFun | IRTS.Defunctionalise |
| DHide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Dictionary | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dictionary | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DInclude | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Directive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| directive | Idris.Parser |
| directiveAction | Idris.Directives |
| disallowImp | Idris.Parser.Expr, Idris.Parser |
| disamb | Idris.Parser.Expr, Idris.Parser |
| discard | Idris.Core.TT |
| DLanguage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DLet | IRTS.Defunctionalise |
| DLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DLink | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DLogging | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DNameHint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DNothing | IRTS.Defunctionalise |
| DoBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| DoBindP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| doBlock | Idris.Parser.Expr, Idris.Parser |
| docComment | Idris.Parser.Helpers, 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 |
| 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.Parser.Expr, Idris.Parser |
| do_alt | Idris.Parser.Expr, 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.Parser.Data, 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 |
| DumpHighlights | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| dumpprobs | Idris.Core.Elaborate |
| dumpTT | Idris.AbsSyntax |
| DUpdate | IRTS.Defunctionalise |
| DUsed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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_name_fc | 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 |
| EAbandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ECheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EDefns | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Edit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EDocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EEval | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eEVAL | IRTS.Defunctionalise |
| EInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eInfoNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EitherErr | Idris.AbsSyntax |
| Elab | Idris.Core.Elaborate |
| elab | Idris.Elab.Term |
| Elab' | Idris.Core.Elaborate |
| elabCaseBlock | Idris.Elab.Utils |
| elabCats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elabClass | Idris.Elab.Class |
| elabClause | Idris.Elab.Clause |
| elabClauses | Idris.Elab.Clause |
| ElabCtxt | |
| 1 (Type/Class) | Idris.Elab.Term |
| 2 (Data Constructor) | Idris.Elab.Term |
| ElabD | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elabData | Idris.Elab.Data |
| elabDecl | Idris.ElabDecls |
| elabDecl' | Idris.ElabDecls |
| elabDecls | Idris.ElabDecls |
| elabDocTerms | Idris.Elab.Value |
| elabExec | Idris.Elab.Value |
| elabExtern | Idris.Elab.Type |
| elabFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ElabInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| elabInstance | Idris.Elab.Instance |
| elabMain | Idris.ElabDecls |
| ElabMode | Idris.Elab.Term |
| elaborate | Idris.Core.Elaborate |
| Elaborating | Idris.Core.TT |
| ElaboratingArg | Idris.Core.TT |
| elaboratingArgErr | Idris.Elab.Term |
| elaborating_app | Idris.Core.Elaborate |
| elabPE | Idris.Elab.Clause |
| elabPostulate | Idris.Elab.Type |
| elabPrims | Idris.ElabDecls |
| elabProvider | Idris.Elab.Provider |
| elabRecord | Idris.Elab.Record |
| elabREPL | Idris.Elab.Value |
| ElabResult | |
| 1 (Type/Class) | Idris.Elab.Term |
| 2 (Data Constructor) | Idris.Elab.Term |
| elabRunElab | Idris.Elab.RunElab |
| ElabScriptDebug | Idris.Core.TT |
| ElabScriptStaging | Idris.Core.TT |
| ElabScriptStuck | Idris.Core.TT |
| ElabShellCmd | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ElabState | Idris.Core.Elaborate |
| 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.Elab.Term |
| 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 |
| envlen | Idris.Core.TT |
| EnvTT | Idris.Core.TT |
| envTupleType | Idris.Reflection |
| eol | Idris.Parser.Helpers, Idris.Parser |
| EProofState | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EProofTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EQED | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqParamDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| eqProp | Idris.Parser.Helpers, 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 |
| erasure | Idris.Reflection |
| ErasureInfo | Idris.Core.CaseTree |
| ERHS | Idris.Elab.Term |
| 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 |
| ESearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EState | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ETransLHS | Idris.Elab.Term |
| ETyDecl | Idris.Elab.Term |
| ETypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| EUndo | 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 |
| EvalTypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| ExactlyOne | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Example | Idris.Docstrings |
| execElab | Idris.Core.Elaborate |
| Executable | IRTS.CodegenCommon |
| Execute | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| execute | Idris.Core.Execute |
| ExecVal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Exp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ExpandLet | Idris.Core.ProofState, Idris.Core.Elaborate |
| expandLet | Idris.Core.Elaborate |
| expandNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| expandParams | Idris.AbsSyntax |
| expandParamsD | Idris.AbsSyntax |
| expandSugar | Idris.DSL |
| expArg | Idris.AbsSyntax |
| ExpectedType | Idris.Core.TT |
| expl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| explicit | Idris.Core.Elaborate |
| ExplicitD | Idris.PartialEval |
| explicitNames | Idris.Core.TT |
| explicitPi | Idris.Parser.Expr, Idris.Parser |
| 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.Parser.Expr, Idris.Parser |
| expr' | Idris.Parser.Expr, Idris.Parser |
| ExprArg | Idris.Help |
| ExprTArg | Idris.Parser.Expr, Idris.Parser |
| Extension | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| extension | Idris.Parser.Expr, Idris.Parser |
| extensions | Idris.Parser.Expr, Idris.Parser |
| externalDecl | Idris.Parser |
| externalExpr | Idris.Parser.Expr, Idris.Parser |
| ExternalIO | Idris.Core.Evaluate |
| extractUnquotes | Idris.Elab.Quasiquote |
| extraHelp | Idris.Help |
| e_guarded | Idris.Elab.Term |
| e_inarg | Idris.Elab.Term |
| e_intype | Idris.Elab.Term |
| e_isfn | Idris.Elab.Term |
| e_nomatching | Idris.Elab.Term |
| e_qq | Idris.Elab.Term |
| FailAt | Idris.Core.Unify |
| FailContext | |
| 1 (Type/Class) | Idris.Core.Unify |
| 2 (Data Constructor) | Idris.Core.Unify |
| Failing | Idris.Docstrings |
| 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 |
| FancyMsg | Idris.Core.TT |
| 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 |
| FCData | IRTS.Lang, IRTS.Defunctionalise |
| fcIn | Idris.Core.TT |
| 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 |
| fgetState | Idris.ASTUtils |
| Field | Idris.ASTUtils |
| FileArg | Idris.Help |
| FileFC | Idris.Core.TT |
| fileFC | Idris.Core.TT |
| Filename | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fileName | Idris.Parser.Helpers, 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 |
| findHighlight | Idris.Elab.Term |
| findImport | Idris.Imports |
| findInPath | Idris.Imports |
| findParams | Idris.Elab.Utils |
| findPkgIndex | Idris.Imports |
| findStatics | Idris.AbsSyntax |
| findUnique | Idris.Elab.Clause |
| findUsedArgs | Idris.Core.CaseTree |
| FIO | IRTS.Lang, IRTS.Defunctionalise |
| FirstSuccess | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Fix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixColour | Idris.Parser |
| FixDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixErrorMsg | Idris.Parser.Helpers, Idris.Parser |
| Fixity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| fixity | Idris.Parser.Ops, Idris.Parser |
| fixityType | Idris.Parser.Ops, Idris.Parser |
| Fl | Idris.Core.TT |
| float | Idris.Parser.Helpers, Idris.Parser |
| FManagedPtr | IRTS.Lang, IRTS.Defunctionalise |
| fmapMB | Idris.Core.TT |
| 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.Parser.Ops, 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 |
| forceDefCtxt | Idris.Core.DeepSeq, Idris.DeepSeq |
| 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.Reflection |
| Frozen | Idris.Core.Evaluate |
| 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.Parser.Expr, Idris.Parser |
| fullTactic | Idris.Parser.Expr, 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 |
| Generated | Idris.Core.Evaluate |
| generateDocs | Idris.IdrisDoc |
| getAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getAllNames | Idris.AbsSyntax |
| getArgs | Idris.Reflection |
| getArgTys | Idris.Core.TT |
| getAutoHints | Idris.AbsSyntax |
| getAutoImpls | Idris.AbsSyntax |
| getAutoImports | Idris.AbsSyntax |
| getAux | Idris.Core.Elaborate |
| getCC | IRTS.System |
| getClause | Idris.CaseSplit |
| getClient | Idris.REPL |
| getCmdLine | Idris.AbsSyntax |
| getCoercionsTo | Idris.AbsSyntax |
| getConsts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getContext | Idris.AbsSyntax |
| getDataDir | IRTS.System |
| getDataFileName | IRTS.System |
| getDefinedNames | Idris.AbsSyntax |
| getDeprecated | Idris.AbsSyntax |
| getDesugarNats | Idris.AbsSyntax |
| getDocs | Idris.Docs |
| getDumpCases | Idris.AbsSyntax |
| getDumpDefun | Idris.AbsSyntax |
| getDumpHighlighting | Idris.AbsSyntax |
| getEnvFlags | IRTS.System |
| getErasureInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getErasureUsage | Idris.AbsSyntax |
| getErrSpan | Idris.Error |
| getExpNames | IRTS.Exports |
| getExports | Idris.AbsSyntax |
| getExps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getFC | Idris.Parser.Helpers, Idris.Parser |
| getFixedInType | Idris.Elab.Utils |
| getFlags | Idris.AbsSyntax |
| getFlexInType | Idris.Elab.Utils |
| getFn | IRTS.Defunctionalise |
| getFromHideList | Idris.AbsSyntax |
| getFunctionErrorHandlers | Idris.AbsSyntax |
| getHdrs | Idris.AbsSyntax |
| getIdrisLibDir | IRTS.System |
| GetIdrisVersion | Idris.IdeMode |
| getImported | Idris.AbsSyntax |
| getImports | Idris.Chaser |
| getImps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getIncFlags | IRTS.System |
| getInferTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getInferType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getInternalApp | Idris.AbsSyntax |
| getIState | Idris.AbsSyntax |
| getLastTokenSpan | Idris.Parser.Helpers, Idris.Parser |
| getLen | Idris.IdeMode |
| getLibFlags | IRTS.System |
| getLibs | Idris.AbsSyntax |
| getLog | Idris.Core.Elaborate |
| getModuleFiles | Idris.Chaser |
| getName | Idris.AbsSyntax |
| getNameFrom | Idris.Core.Elaborate |
| getNameHints | Idris.AbsSyntax |
| getNChar | Idris.IdeMode |
| getNextName | IRTS.Lang, IRTS.Defunctionalise |
| getNoBanner | Idris.AbsSyntax |
| getObjectFiles | Idris.AbsSyntax |
| getOptimise | Idris.AbsSyntax |
| GetOpts | Idris.IdeMode |
| getParamsInType | Idris.Elab.Utils |
| getPArity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getPBtys | Idris.Elab.Utils |
| getPkg | Idris.REPL |
| getPkgCheck | Idris.REPL |
| getPkgClean | 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 |
| getPSnames | Idris.Core.Elaborate |
| 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 |
| getTCinj | Idris.Elab.Utils |
| getTCParamsInType | Idris.Elab.Utils |
| getTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| getTotality | Idris.AbsSyntax |
| getUnboundImplicits | Idris.AbsSyntax |
| getUndefined | Idris.AbsSyntax |
| getUnifyLog | Idris.Core.Elaborate |
| getUniq | Idris.CaseSplit |
| getUniqueUsed | Idris.Elab.Utils |
| getUnmatchable | Idris.Elab.Term |
| getWidth | Idris.AbsSyntax |
| get_autos | Idris.Core.Elaborate |
| get_context | Idris.Core.Elaborate |
| get_datatypes | Idris.Core.Elaborate |
| get_deferred | Idris.Core.Elaborate |
| get_dotterm | Idris.Core.Elaborate |
| get_env | Idris.Core.Elaborate |
| get_global_nextname | 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 |
| get_usedns | Idris.Core.Elaborate |
| GHole | Idris.Core.TT |
| GivenVal | Idris.Core.TT |
| Glob | IRTS.Lang, IRTS.Defunctionalise |
| global_nextname | Idris.Core.ProofState, Idris.Core.Elaborate |
| 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.Elab.Term |
| groupsOf | IRTS.Defunctionalise |
| gteProp | Idris.Parser.Helpers, Idris.Parser |
| gtProp | Idris.Parser.Helpers, Idris.Parser |
| Guarded | Idris.Coverage |
| Guardedness | Idris.Coverage |
| Guess | Idris.Core.TT |
| handleError | Idris.Core.Elaborate |
| HasLastTokenSpan | Idris.Parser.Helpers, Idris.Parser |
| hasValidIBCVersion | Idris.IBC |
| Header | Idris.Docstrings |
| Help | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| help | Idris.REPL.Parser |
| hEndColourise | Idris.Colours |
| Hidden | Idris.Core.Evaluate |
| HideDisplay | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| hide_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| highestFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| highlighting | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| highlightP | Idris.Parser.Helpers, Idris.Parser |
| highlightSource | 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.TT |
| holes | Idris.Core.ProofState, Idris.Core.Elaborate |
| HowMuchDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| HRule | Idris.Docstrings |
| hsimpleExpr | Idris.Parser.Expr, Idris.Parser |
| hStartColourise | Idris.Colours |
| HtmlBlock | Idris.Docstrings |
| HTMLOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| hWriteDoc | Idris.Output |
| I | Idris.Core.TT |
| IBC | Idris.Imports |
| IBCAccess | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCAutoHint | 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 |
| IBCDeprecate | 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 |
| IBCExtern | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| ibcPathNoFallback | Idris.Imports |
| IBCPhase | Idris.IBC |
| IBCPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBCRecord | 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 |
| IBCWrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IBC_Building | Idris.IBC |
| IBC_REPL | Idris.IBC |
| ibc_write | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ICodeGen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ICoverage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdeMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Idemode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IdeModeCommand | Idris.IdeMode |
| ideModeEpoch | Idris.IdeMode |
| idemodePutSExp | Idris.Output |
| ideModeReturnAnnotated | Idris.Output |
| ideModeReturnWithStatus | Idris.Output |
| IdemodeSocket | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| identifier | Idris.Parser.Helpers, Idris.Parser |
| iderr | Idris.Elab.Utils |
| idiom | Idris.Parser.Expr, 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.Parser.Helpers, Idris.Parser |
| 2 (Data Constructor) | Idris.Parser.Helpers, Idris.Parser |
| idrisMain | Idris.REPL |
| IdrisParser | Idris.Parser.Helpers, Idris.Parser |
| idrisStyle | Idris.Parser.Helpers, Idris.Parser |
| idris_autohints | 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_deprecated | 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_externs | 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_highlightedRegions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_implicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_infixes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_inmodule | 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_parserHighlights | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_patdefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_postulates | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_records | 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_ttstats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_tyinfodata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| idris_whocalls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IElab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IErasure | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ierror | Idris.Error |
| ifail | Idris.Error |
| IFileType | Idris.Imports |
| if_ | Idris.Parser.Expr, Idris.Parser |
| IIBC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Image | Idris.Docstrings |
| Imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| impIn | 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.Parser.Expr, Idris.Parser |
| ImplicitColour | Idris.Colours |
| implicitColour | Idris.Colours |
| ImplicitD | Idris.PartialEval |
| ImplicitInfo | Idris.Core.TT |
| implicitise | Idris.AbsSyntax |
| implicitNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| implicitPi | Idris.Parser.Expr, Idris.Parser |
| ImplicitS | Idris.PartialEval |
| ImportDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| importDirs | IRTS.CodegenCommon |
| imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ImportInfo | |
| 1 (Type/Class) | Idris.Parser |
| 2 (Data Constructor) | Idris.Parser |
| import_ | Idris.Parser |
| import_location | Idris.Parser |
| import_modname_location | Idris.Parser |
| import_namespace | Idris.Parser |
| import_path | Idris.Parser |
| import_reexport | Idris.Parser |
| import_rename | Idris.Parser |
| Impossible | Idris.Core.TT |
| impossible | Idris.Parser.Expr, Idris.Parser |
| 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.Parser.Helpers, Idris.Parser |
| inblock | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| includes | IRTS.CodegenCommon |
| IncompleteTerm | Idris.Core.TT |
| indent | |
| 1 (Function) | IRTS.DumpBC |
| 2 (Function) | Idris.Parser.Helpers, Idris.Parser |
| indented | Idris.Parser.Helpers, Idris.Parser |
| indentedBlock | Idris.Parser.Helpers, Idris.Parser |
| indentedBlock1 | Idris.Parser.Helpers, Idris.Parser |
| indentedBlockS | Idris.Parser.Helpers, Idris.Parser |
| IndentProperty | |
| 1 (Type/Class) | Idris.Parser.Helpers, Idris.Parser |
| 2 (Data Constructor) | Idris.Parser.Helpers, Idris.Parser |
| indentPropHolds | Idris.Parser.Helpers, 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 |
| infer_app | Idris.Core.Elaborate |
| 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.Elab.Term |
| initElaborator | Idris.Core.Elaborate |
| initEState | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| initEval | Idris.Core.Evaluate |
| initNextNameFrom | Idris.Core.Elaborate |
| initsEndAt | Idris.Parser.Helpers, 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 |
| inPkgDir | Pkg.Package |
| 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 |
| instanceCtorName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| InstanceN | Idris.Core.TT |
| instances | Idris.Core.ProofState, Idris.Core.Elaborate |
| instance_ | Idris.Parser |
| instantiate | Idris.Core.TT |
| integer | Idris.Parser.Helpers, Idris.Parser |
| IntegerAtom | Idris.IdeMode |
| integerReader | Idris.CmdOptions |
| Interface | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| interfaces | IRTS.CodegenCommon |
| interMap | IRTS.DumpBC |
| internalDecl | Idris.Parser |
| internalExpr | Idris.Parser.Expr, 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 |
| intToReflectedNat | Idris.Reflection |
| IntTy | Idris.Core.TT |
| intTyName | Idris.Core.TT |
| invalidOperators | Idris.Parser.Helpers, Idris.Parser |
| InvalidTCArg | Idris.Core.TT |
| IOption | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| IParse | 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 |
| isATTY | Util.System |
| isConName | Idris.Core.Evaluate |
| isConst | IRTS.Bytecode |
| isDConName | Idris.Core.Evaluate |
| isEol | Idris.Parser.Helpers, 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 |
| isPlausible | Idris.Elab.Term |
| 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 |
| ITChar | Idris.Core.TT |
| ITFixed | Idris.Core.TT |
| ITNative | Idris.Core.TT |
| Itself | Idris.Core.Evaluate |
| 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 |
| JSClear | IRTS.JavaScript.AST |
| JSCond | IRTS.JavaScript.AST |
| JSConstructor | IRTS.JavaScript.AST |
| JSDelete | 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.Parser.Helpers, 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 |
| LAlt | IRTS.Lang, IRTS.Defunctionalise |
| LAlt' | IRTS.Lang, IRTS.Defunctionalise |
| Lam | Idris.Core.TT |
| lambda | Idris.Parser.Expr, Idris.Parser |
| lambdaLift | IRTS.Lang, IRTS.Defunctionalise |
| LAnd | IRTS.Lang, IRTS.Defunctionalise |
| LanguageExt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LApp | IRTS.Lang, IRTS.Defunctionalise |
| LASHR | IRTS.Lang, IRTS.Defunctionalise |
| lastIndent | Idris.Parser.Helpers, 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.Parser.Helpers, Idris.Parser |
| lcharFC | Idris.Parser.Helpers, 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.Parser.Expr, Idris.Parser |
| let_binding | Idris.Parser.Expr, Idris.Parser |
| LExp | IRTS.Lang, IRTS.Defunctionalise |
| LExternal | 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 |
| lift | IRTS.Lang, IRTS.Defunctionalise |
| liftAll | IRTS.Lang, IRTS.Defunctionalise |
| liftDecls | IRTS.CodegenCommon |
| liftname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| liftPats | Idris.Core.TT |
| LiftState | IRTS.Lang, IRTS.Defunctionalise |
| LineBreak | Idris.Docstrings |
| lineNum | Idris.Parser.Helpers, 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.Parser.Expr, Idris.Parser |
| 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 |
| lname | IRTS.Lang, IRTS.Defunctionalise |
| LNoOp | IRTS.Lang, IRTS.Defunctionalise |
| LNothing | 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 |
| localnames | Idris.Core.TT |
| LogCat | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| LogCategory | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| logCodeGen | Idris.AbsSyntax |
| logCoverage | Idris.AbsSyntax |
| logElab | Idris.AbsSyntax |
| logErasure | Idris.AbsSyntax |
| loggingCatsStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| logIBC | Idris.AbsSyntax |
| logLevel | Idris.AbsSyntax |
| LogLvl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| logLvl | Idris.AbsSyntax |
| logLvlCats | Idris.AbsSyntax |
| logParser | Idris.AbsSyntax |
| lookAheadMatches | Idris.Parser.Helpers, 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 |
| lookupTotalExact | 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 |
| LPlus | IRTS.Lang, IRTS.Defunctionalise |
| LProj | IRTS.Lang, IRTS.Defunctionalise |
| LReadStr | IRTS.Lang, IRTS.Defunctionalise |
| LS | IRTS.Lang, IRTS.Defunctionalise |
| LSDiv | IRTS.Lang, IRTS.Defunctionalise |
| LSExt | IRTS.Lang, IRTS.Defunctionalise |
| LSGe | IRTS.Lang, IRTS.Defunctionalise |
| LSGt | IRTS.Lang, IRTS.Defunctionalise |
| LSHL | IRTS.Lang, IRTS.Defunctionalise |
| LSLe | IRTS.Lang, IRTS.Defunctionalise |
| LSLt | IRTS.Lang, IRTS.Defunctionalise |
| LSRem | 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 |
| LStrSubstr | IRTS.Lang, IRTS.Defunctionalise |
| LStrTail | IRTS.Lang, IRTS.Defunctionalise |
| LSystemInfo | IRTS.Lang, IRTS.Defunctionalise |
| lteProp | Idris.Parser.Helpers, Idris.Parser |
| LTimes | IRTS.Lang, IRTS.Defunctionalise |
| ltProp | Idris.Parser.Helpers, Idris.Parser |
| LTrunc | IRTS.Lang, IRTS.Defunctionalise |
| LUDiv | IRTS.Lang, IRTS.Defunctionalise |
| LURem | IRTS.Lang, IRTS.Defunctionalise |
| LV | IRTS.Lang, IRTS.Defunctionalise |
| LVar | 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 |
| MakeCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| makeCase | Idris.Interactive |
| MakeCaseBlock | Idris.IdeMode |
| 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 |
| Many | Idris.Core.Typecheck |
| ManyArgs | Idris.Help |
| mapCtxt | Idris.Core.TT |
| mapDefCtxt | Idris.Core.Evaluate |
| mapPDataFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapPDeclFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapPT | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapPTermFC | 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 |
| MaybeHoles | Idris.Core.TT |
| maybeWithNS | Idris.Parser.Helpers, Idris.Parser |
| MetaInformation | Idris.Core.Evaluate |
| MetaN | Idris.Core.TT |
| MetaVarArg | Idris.Help |
| Metavariables | Idris.IdeMode |
| metavarName | Idris.Elab.Term |
| 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 |
| mkList | Idris.Reflection |
| mkMultiPaths | Idris.Coverage |
| mkName | Idris.Parser.Helpers, Idris.Parser |
| mkPApp | Idris.AbsSyntax |
| mkPatTm | Idris.Coverage |
| mkPE_TermDecl | Idris.PartialEval |
| mkPE_TyDecl | Idris.PartialEval |
| mkProofTerm | Idris.Core.ProofTerm |
| mkStatic | Idris.Elab.Utils |
| mkStaticTy | Idris.Elab.Utils |
| mkTTName | Idris.DSL |
| mkType | Idris.Parser.Expr, 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.Parser.Expr, 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.Parser.Helpers, 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.Parser.Helpers, Idris.Parser |
| MultiPath | Idris.Coverage |
| Mutual | Idris.Core.Evaluate |
| mutual | Idris.Parser |
| mutual_types | Idris.Core.TT |
| mut_nesting | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Name | Idris.Core.TT |
| name | Idris.Parser.Helpers, Idris.Parser |
| NameArg | Idris.Help |
| NamedInstanceDoc | Idris.Docs |
| nameMissing | Idris.CaseSplit |
| NameOutput | Idris.Core.TT |
| NamePart | Idris.Core.TT |
| namequote | Idris.Parser.Expr, Idris.Parser |
| nameRoot | Idris.CaseSplit |
| namesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| namesInNS | Idris.REPL.Browse |
| namespace | |
| 1 (Function) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Function) | Idris.Parser |
| NamespaceArg | Idris.Help |
| namespacesInNS | Idris.REPL.Browse |
| namesUsed | Idris.Core.CaseTree |
| NameTArg | Idris.Parser.Expr, Idris.Parser |
| NameType | Idris.Core.TT |
| Native | IRTS.Lang, IRTS.Defunctionalise |
| NativeTy | Idris.Core.TT |
| nativeTyWidth | Idris.Core.TT |
| natural | Idris.Parser.Helpers, Idris.Parser |
| 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.Parser.Helpers, Idris.Parser |
| noDocs | Idris.Docstrings |
| NoElimDeprecationWarnings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| NoEliminator | Idris.Core.TT |
| noErrors | Idris.AbsSyntax |
| NoFC | Idris.Core.TT |
| nofixityoperator | Idris.Parser.Ops, Idris.Parser |
| NoImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| noImplicits | Idris.Parser.Expr, Idris.Parser |
| NoInline | IRTS.Lang, IRTS.Defunctionalise |
| NonCollapsiblePostulate | Idris.Core.TT |
| NONE | IRTS.CodegenCommon |
| NonFunctionType | Idris.Core.TT |
| noOccurrence | Idris.Core.TT |
| NoOldTacticDeprecationWarnings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| normalImplicit | Idris.Parser.Expr, Idris.Parser |
| normalise | Idris.Core.Evaluate |
| normaliseAll | Idris.Core.Evaluate |
| normaliseBlocking | Idris.Core.Evaluate |
| normaliseC | Idris.Core.Evaluate |
| normaliseTrace | Idris.Core.Evaluate |
| NoSuchVariable | Idris.Core.TT |
| NotCovering | Idris.Core.Evaluate |
| notEndApp | Idris.Parser.Helpers, Idris.Parser |
| notEndBlock | Idris.Parser.Helpers, Idris.Parser |
| NotEquality | Idris.Core.TT |
| NotInjective | Idris.Core.TT |
| notOpenBraces | Idris.Parser.Helpers, Idris.Parser |
| NotPositive | Idris.Core.Evaluate |
| NotProductive | Idris.Core.Evaluate |
| notunified | Idris.Core.ProofState, Idris.Core.Elaborate |
| NoTypeDecl | Idris.Core.TT |
| NoValidAlts | 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 |
| OLogCats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OLogging | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Once | Idris.Core.Typecheck |
| OP | IRTS.Bytecode |
| opChars | Idris.Parser.Helpers, Idris.Parser |
| openBlock | Idris.Parser.Helpers, Idris.Parser |
| Operator | Idris.Core.Evaluate |
| operator | Idris.Parser.Helpers, Idris.Parser |
| operatorFC | Idris.Parser.Helpers, Idris.Parser |
| operatorFront | Idris.Parser.Ops, Idris.Parser |
| operatorLetter | Idris.Parser.Helpers, Idris.Parser |
| opExpr | Idris.Parser.Expr, Idris.Parser |
| Opt | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Type/Class) | Idris.IdeMode |
| opt | Idris.REPL |
| Optimisation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Optimise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OptInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| OptionalArg | Idris.Help |
| OptionArg | Idris.Help |
| OptLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opts_idrisCmdline | Idris.ASTUtils |
| opt_autoimpls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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_desugarnats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_detaggable | Idris.ASTUtils |
| opt_errContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_evaltypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_ibcsubdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_importdirs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| opt_inaccessible | Idris.ASTUtils |
| opt_logcats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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_printdepth | 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.Parser.Data, Idris.Parser |
| Overview | Idris.IdeMode |
| overview | Idris.Docstrings |
| OverviewDocs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| P | Idris.Core.TT |
| pairCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pairTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAlternative | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAltType | 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.Core.TT |
| ParentN | Idris.Core.TT |
| PArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PArg' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pargopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parseCmd | Idris.REPL.Parser |
| parseCodegen | Idris.CmdOptions |
| parseConsoleWidth | Idris.CmdOptions |
| parseConst | Idris.Parser |
| parseDocstring | Idris.Docstrings |
| parseElabShellStep | Idris.Parser |
| parseExpr | Idris.Parser |
| parseFlags | Idris.CmdOptions |
| parseImports | Idris.Parser |
| parseLogCats | Idris.CmdOptions |
| parseMessage | Idris.IdeMode |
| parseProg | Idris.Parser |
| parser | Idris.CmdOptions |
| parserCats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parserWarning | Idris.Parser.Helpers, Idris.Parser |
| 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 |
| patvar' | Idris.Core.Elaborate |
| pbinds | Idris.Elab.Utils |
| pbty | Idris.Elab.Utils |
| PCAF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| pconst | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstant | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstSugar | 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 |
| PDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDecl' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| PDPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PEArgType | Idris.PartialEval |
| PEGenerated | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PElabError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pEraseType | Idris.Core.TT |
| performUsageAnalysis | Idris.Erasure |
| PETransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pexp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pe_app | Idris.PartialEval |
| pe_clauses | Idris.PartialEval |
| pe_def | Idris.PartialEval |
| pe_simple | Idris.PartialEval |
| PFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PGoal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Phase | Idris.Core.CaseTree |
| PHidden | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Pi | Idris.Core.TT |
| pi | Idris.Parser.Expr, Idris.Parser |
| piBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| piBindp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PIdiom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PIfThenElse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PImpossible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PInferRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| piOpts | Idris.Parser.Expr, Idris.Parser |
| 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 |
| Plicity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| plog | Idris.Core.ProofState, Idris.Core.Elaborate |
| pmap | Idris.Core.TT |
| PMatchApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMutual | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PNamespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PNoImplicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| popIndent | Idris.Parser.Helpers, Idris.Parser |
| 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 |
| 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_depth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ppopt_desugarnats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ppopt_impl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ppopt_pinames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPrint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pprintConstDocs | Idris.Docs |
| pprintDelab | Idris.Delaborate |
| pprintDelabTy | Idris.Delaborate |
| pprintDocs | Idris.Docs |
| pprintErr | Idris.Delaborate |
| pprintNoDelab | Idris.Delaborate |
| pprintPTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pprintRaw | Idris.Core.TT |
| pprintTT | Idris.Core.TT |
| pprintTypeDoc | Idris.Docs |
| PProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProvider | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuasiquote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuoteName | 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.Parser.Ops, Idris.Parser |
| PrefixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| Private | Idris.Core.Evaluate |
| problems | Idris.Core.ProofState, Idris.Core.Elaborate |
| processTactic | Idris.Core.ProofState, Idris.Core.Elaborate |
| processTactic' | Idris.Core.Elaborate |
| processTacticDecls | Idris.Elab.Term |
| 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.Parser.Expr, Idris.Parser |
| proofFail | Idris.Core.Elaborate |
| Proofs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ProofSearch | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| proofSearch | Idris.ProofSearch |
| proofSearch' | Idris.Elab.Term |
| 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 |
| Provenance | Idris.Core.TT |
| prover | Idris.Prover |
| proverCompletion | Idris.Completion |
| 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.Elab.Term |
| pruneByType | Idris.Elab.Term |
| PRunElab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRunElabDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prunStateT | Idris.Core.Elaborate |
| PS | Idris.Core.ProofState, Idris.Core.Elaborate |
| pscoped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pscript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pshow | Idris.Output |
| psnames | Idris.Core.ProofState, Idris.Core.Elaborate |
| psolve | Idris.Elab.Utils |
| pstatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| psubst | Idris.Core.TT |
| PSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| pToV | Idris.Core.TT |
| pToVs | Idris.Core.TT |
| PTransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| pushIndent | Idris.Parser.Helpers, 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.Parser.Expr, Idris.Parser |
| Quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Quote | Idris.Core.Evaluate |
| quote | Idris.Core.Evaluate |
| quoteGoal | Idris.Parser.Expr, Idris.Parser |
| quoteTerm | Idris.Core.Evaluate |
| RAddInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RApp | Idris.Core.TT |
| rArgOpts | Idris.Reflection |
| Raw | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| rawBool | Idris.Reflection |
| rawCons | Idris.Reflection |
| RawHtml | Idris.Docstrings |
| rawList | Idris.Reflection |
| rawNil | Idris.Reflection |
| RawOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| rawPair | Idris.Reflection |
| rawPairTy | Idris.Reflection |
| RawPart | Idris.Core.TT |
| rawTriple | Idris.Reflection |
| rawTripleTy | Idris.Reflection |
| raw_apply | Idris.Core.TT |
| raw_unapply | Idris.Core.TT |
| RBind | Idris.Core.TT |
| RClausesInstrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RConstant | Idris.Core.TT |
| RConstraint | Idris.Reflection |
| RConstructor | Idris.Reflection |
| RConstructorDefn | Idris.Reflection |
| RCtorArg | Idris.Reflection |
| RCtorField | Idris.Reflection |
| RCtorParameter | Idris.Reflection |
| RDataDefn | Idris.Reflection |
| RDatatype | |
| 1 (Type/Class) | Idris.Reflection |
| 2 (Data Constructor) | Idris.Reflection |
| RDatatypeDeclInstrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RDatatypeDefnInstrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RDeclare | Idris.Reflection |
| RDeclInstructions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RDefineDatatype | Idris.Reflection |
| RDefineFun | Idris.Reflection |
| readSource | Util.System |
| REBASE | IRTS.Bytecode |
| 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.Parser.Data, Idris.Parser |
| RecordDoc | Idris.Docs |
| recordI | Idris.Parser.Data, Idris.Parser |
| RecordInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| recordParameter | Idris.Parser.Data, Idris.Parser |
| recordType | Idris.Parser.Expr, Idris.Parser |
| record_constructor | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| record_parameters | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| record_projections | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| recoverableCoverage | Idris.Coverage |
| rec_elabDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ref | Idris.Core.TT |
| Refine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflCall | Idris.Reflection |
| Reflect | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| reflect | Idris.Reflection |
| reflectArg | Idris.Reflection |
| reflectBinder | Idris.Reflection |
| reflectBinderQuote | Idris.Reflection |
| reflectBinderQuotePattern | Idris.Reflection |
| reflectConstant | Idris.Reflection |
| reflectCtorArg | Idris.Reflection |
| reflectCtxt | Idris.Reflection |
| reflectDatatype | Idris.Reflection |
| reflectEnv | Idris.Reflection |
| reflectErasure | Idris.Reflection |
| reflectErr | Idris.Reflection |
| reflectFC | Idris.Reflection |
| reflectFixity | Idris.Reflection |
| reflectFunClause | Idris.Reflection |
| reflectFunDefn | Idris.Reflection |
| Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ReflectionError | Idris.Core.TT |
| ReflectionFailed | Idris.Core.TT |
| reflectList | Idris.Reflection |
| reflectName | Idris.Reflection |
| reflectNameQuotePattern | Idris.Reflection |
| reflectNameType | Idris.Reflection |
| reflectPlicity | Idris.Reflection |
| reflectRaw | Idris.Reflection |
| reflectRawQuote | Idris.Reflection |
| reflectRawQuotePattern | Idris.Reflection |
| reflectSpecialName | Idris.Reflection |
| reflectTTQuote | Idris.Reflection |
| reflectTTQuotePattern | Idris.Reflection |
| reflectUExp | Idris.Reflection |
| reflectUniverse | Idris.Reflection |
| reflErrName | Idris.Reflection |
| reflm | Idris.Reflection |
| 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.Reflection |
| reifyApp | Idris.Reflection |
| reifyArithTy | Idris.Reflection |
| reifyBool | Idris.Reflection |
| reifyEnv | Idris.Reflection |
| reifyErasure | Idris.Reflection |
| reifyFC | Idris.Reflection |
| reifyFunDefn | Idris.Reflection |
| reifyInt | Idris.Reflection |
| reifyIntTy | Idris.Reflection |
| reifyList | Idris.Reflection |
| reifyNativeTy | Idris.Reflection |
| reifyPair | Idris.Reflection |
| reifyPlicity | Idris.Reflection |
| reifyRaw | Idris.Reflection |
| reifyRawApp | Idris.Reflection |
| reifyRConstructorDefn | Idris.Reflection |
| reifyRDataDefn | Idris.Reflection |
| reifyReportPart | Idris.Reflection |
| reifyReportParts | Idris.Reflection |
| reifyRFunArg | Idris.Reflection |
| reifyTT | Idris.Reflection |
| reifyTTApp | Idris.Reflection |
| reifyTTBinder | Idris.Reflection |
| reifyTTBinderApp | Idris.Reflection |
| reifyTTConst | Idris.Reflection |
| reifyTTConstApp | Idris.Reflection |
| reifyTTName | Idris.Reflection |
| reifyTTNameApp | Idris.Reflection |
| reifyTTNamespace | Idris.Reflection |
| reifyTTNameType | Idris.Reflection |
| reifyTTUExp | Idris.Reflection |
| reifyTyDecl | Idris.Reflection |
| reifyUniverse | Idris.Reflection |
| Reload | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RemoveOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| removeOptimise | Idris.AbsSyntax |
| renderDocstring | Idris.Docstrings |
| renderDocTerm | Idris.Docstrings |
| renderExternal | Idris.Output |
| renderHtml | Idris.Docstrings |
| Reorder | Idris.Core.ProofState, Idris.Core.Elaborate |
| reorder_claims | Idris.Core.Elaborate |
| replaceSplits | Idris.CaseSplit |
| replCompletion | Idris.Completion |
| REPLCompletions | Idris.IdeMode |
| replPkg | Pkg.Package |
| repl_definitions | Idris.ASTUtils |
| report | Idris.Error |
| reportParserWarnings | Idris.Parser.Helpers, Idris.Parser |
| RErased | Idris.Reflection |
| RErasure | Idris.Reflection |
| RESERVE | IRTS.Bytecode |
| reserved | Idris.Parser.Helpers, Idris.Parser |
| reservedFC | Idris.Parser.Helpers, Idris.Parser |
| reservedHL | Idris.Parser.Helpers, Idris.Parser |
| reservedOp | Idris.Parser.Helpers, Idris.Parser |
| reservedOpFC | Idris.Parser.Helpers, Idris.Parser |
| resetNameIdx | Idris.AbsSyntax |
| resetProofTerm | Idris.Core.ProofTerm |
| resolveTC | Idris.ProofSearch |
| resolveTC' | Idris.Elab.Term |
| resugar | Idris.Delaborate |
| resultCaseDecls | Idris.Elab.Term |
| resultContext | Idris.Elab.Term |
| resultHighlighting | Idris.Elab.Term |
| resultMetavars | Idris.Elab.Term |
| resultName | Idris.Elab.Term |
| resultTerm | Idris.Elab.Term |
| resultTyDecls | Idris.Elab.Term |
| Rewrite | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| rewrite | Idris.Core.Elaborate |
| rewriteTerm | Idris.Parser.Expr, Idris.Parser |
| RExplicit | Idris.Reflection |
| RFunArg | |
| 1 (Type/Class) | Idris.Reflection |
| 2 (Data Constructor) | Idris.Reflection |
| rFunArgToPArg | Idris.Reflection |
| RFunClause | Idris.Reflection |
| RFunDefn | Idris.Reflection |
| rhs | Idris.Parser |
| RI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RightOK | Idris.AbsSyntax |
| RImplicit | Idris.Reflection |
| RIndex | Idris.Reflection |
| rmExe | Pkg.Package |
| rmFile | Util.System |
| rmIBC | Pkg.Package |
| rmIdx | Pkg.Package |
| RMkFunClause | Idris.Reflection |
| RMkImpossibleClause | Idris.Reflection |
| RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RNotErased | Idris.Reflection |
| RParameter | Idris.Reflection |
| RPlicity | Idris.Reflection |
| RTyConArg | Idris.Reflection |
| RTyDecl | Idris.Reflection |
| RTyDeclInstrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RType | Idris.Core.TT |
| rt_simplify | Idris.Core.Evaluate |
| Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| runArgParser | Idris.CmdOptions |
| runClient | Idris.REPL |
| runElab | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.Parser.Expr, Idris.Parser |
| runElabAction | Idris.Elab.Term |
| runElabDecl | Idris.Parser |
| runInnerParser | Idris.Parser.Helpers, Idris.Parser |
| runIO | Idris.AbsSyntax |
| runMain | Idris.REPL |
| RunningElabScript | Idris.Core.TT |
| runparser | Idris.Parser.Helpers, Idris.Parser |
| runTac | Idris.Elab.Term |
| RunTactic' | Idris.Core.ProofTerm |
| 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 |
| 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 |
| SDecl | IRTS.Simplified |
| SDefaultCase | IRTS.Simplified |
| Search | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| searchByType | Idris.TypeSearch |
| searchPred | Idris.TypeSearch |
| sendHighlighting | Idris.Output |
| sendParserHighlighting | Idris.Output |
| 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 |
| setAutoImpls | Idris.AbsSyntax |
| 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 |
| setDepth | Idris.AbsSyntax |
| setDesugarNats | Idris.AbsSyntax |
| setDetaggable | Idris.Elab.Utils |
| setErrContext | Idris.AbsSyntax |
| setErrSpan | Idris.AbsSyntax |
| setEvalTypes | 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 |
| setLogCats | Idris.AbsSyntax |
| 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 |
| setOptions | Idris.REPL.Parser |
| setOptLevel | Idris.AbsSyntax |
| setOutputTy | Idris.AbsSyntax |
| SetPrinterDepth | Idris.AbsSyntaxTree, 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 |
| setupBundledCC | Util.System |
| setVerbose | Idris.AbsSyntax |
| setWidth | Idris.AbsSyntax |
| set_context | Idris.Core.Elaborate |
| set_datatypes | Idris.Core.Elaborate |
| set_global_nextname | Idris.Core.Elaborate |
| SExp | |
| 1 (Type/Class) | IRTS.Simplified |
| 2 (Type/Class) | Idris.IdeMode |
| SExpable | Idris.IdeMode |
| SexpList | Idris.IdeMode |
| sexpToCommand | Idris.IdeMode |
| sExpToString | 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 |
| 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 |
| ShowLoggingCats | 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 |
| showRunElab | Idris.Prover |
| showSep | Idris.Core.TT |
| showTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showTmImpls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| showTmOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| sigmaCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| sigmaTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| simpleCase | Idris.Core.CaseTree |
| simpleConstructor | Idris.Parser.Data, Idris.Parser |
| simpleDecls | IRTS.CodegenCommon |
| SimpleExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| simpleExpr | Idris.Parser.Expr, Idris.Parser |
| simpleExternalExpr | Idris.Parser.Expr, Idris.Parser |
| simpleWhiteSpace | Idris.Parser.Helpers, 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.Parser.Helpers, 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.Elab.Term |
| solveAuto | Idris.Elab.Term |
| solveAutos | Idris.Elab.Term |
| solved | Idris.Core.ProofState, Idris.Core.Elaborate |
| solveDeferred | Idris.AbsSyntax |
| SOp | IRTS.Simplified |
| SourceFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SourceTerm | Idris.Core.TT |
| Space | Idris.Docstrings |
| spanFC | Idris.Core.TT |
| Spec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SpecialHeaderArg | Idris.Help |
| Specialise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| specialise | Idris.Core.Evaluate |
| SpecialName | Idris.Core.TT |
| specType | Idris.PartialEval |
| splitOnLine | Idris.CaseSplit |
| SProj | IRTS.Simplified |
| SSymbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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.Parser.Expr, 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.Parser.Helpers, Idris.Parser |
| StringAtom | Idris.IdeMode |
| stringLiteral | Idris.Parser.Helpers, Idris.Parser |
| StringLitTArg | Idris.Parser.Expr, Idris.Parser |
| stripLinear | Idris.AbsSyntax |
| stripUnmatchable | Idris.AbsSyntax |
| strLogCat | Idris.AbsSyntaxTree, 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.Parser.Helpers, Idris.Parser |
| SymbolAtom | Idris.IdeMode |
| symbolFC | Idris.Parser.Helpers, Idris.Parser |
| SymRef | Idris.Core.TT |
| Syn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SynBind | Idris.Parser.Expr, Idris.Parser |
| SynContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| SynMatch | Idris.Parser.Expr, 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.Parser.Expr, 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.Parser.Ops, Idris.Parser |
| TacImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacimpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacN | Idris.Reflection |
| Tactic | Idris.Core.ProofState, Idris.Core.Elaborate |
| tactic | Idris.Parser.Expr, Idris.Parser |
| TacticArg | Idris.Parser.Expr, Idris.Parser |
| tactics | Idris.Parser.Expr, Idris.Parser |
| tacticsExpr | Idris.Parser.Expr, 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 |
| tcRecoverable | Idris.Elab.Term |
| 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.Parser.Helpers, Idris.Parser |
| TermNoImplicits | Idris.IdeMode |
| TermNormalise | Idris.IdeMode |
| TermPart | Idris.Core.TT |
| TermShowImplicits | Idris.IdeMode |
| TermSize | Idris.Core.TT |
| termsize | Idris.Core.TT |
| termSmallerThan | 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.Core.TT |
| TIData | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| toplevel_imp | Idris.Core.TT |
| toSExp | Idris.IdeMode |
| toTable | Idris.Parser.Ops, 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 |
| toValue | Idris.Core.Evaluate |
| TRACE | IRTS.CodegenCommon |
| traceWhen | Idris.Core.TT |
| transform | Idris.Parser |
| transformErr | Idris.Core.Elaborate |
| TransformInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| transformPats | Idris.Transforms |
| transformPatsWith | Idris.Transforms |
| Trivial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| trivial | Idris.ProofSearch |
| trivial' | Idris.Elab.Term |
| trivialHoles | Idris.ProofSearch |
| trivialHoles' | Idris.Elab.Term |
| Try | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| try | Idris.Core.Elaborate |
| try' | Idris.Core.Elaborate |
| tryAll | Idris.Core.Elaborate |
| tryAll' | Idris.Core.Elaborate |
| tryCatch | Idris.Core.Elaborate |
| tryFullExpr | Idris.Parser.Expr, Idris.Parser |
| TryImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 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 |
| tt_ctxt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| txt | Idris.Core.TT |
| TyDecl | Idris.Core.Evaluate |
| tyOptDeclList | Idris.Parser.Expr, Idris.Parser |
| Type | Idris.Core.TT |
| type1Doc | Idris.AbsSyntax |
| TypeCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TypeColour | Idris.Colours |
| typeColour | Idris.Colours |
| typeDeclList | Idris.Parser.Expr, Idris.Parser |
| typeDescription | Idris.AbsSyntax |
| typeExpr | Idris.Parser.Expr, Idris.Parser |
| TypeInfo | Idris.Core.TT |
| 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 |
| unApplyRaw | Idris.Reflection |
| unboundPi | Idris.Parser.Expr, Idris.Parser |
| 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.Parser.Expr, Idris.Parser |
| unifylog | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifyProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyProblems | Idris.Core.Elaborate |
| UnifyScope | Idris.Core.TT |
| UnifyTerms | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyTerms | Idris.Core.Elaborate |
| 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 |
| UnknownImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UnknownImplicit | Idris.Core.TT |
| unList | Idris.Core.TT |
| unlit | Idris.Unlit |
| UnmatchedCase | Idris.Core.CaseTree |
| unquote | Idris.Parser.Expr, 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 |
| updateSynMatch | Idris.Parser.Expr, Idris.Parser |
| updateSyntaxRules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| update_term | Idris.Core.Elaborate |
| updsubst | Idris.Core.ProofTerm |
| 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 |
| validCoverageCase | Idris.Coverage |
| Value | Idris.Core.Evaluate |
| VApp | Idris.Core.Evaluate |
| Var | Idris.Core.TT |
| var | Idris.DSL |
| VBind | Idris.Core.Evaluate |
| VBLet | Idris.Core.Evaluate |
| VConstant | Idris.Core.Evaluate |
| ver | Idris.REPL |
| VErased | Idris.Core.Evaluate |
| verbatimStringLiteral | Idris.Parser.Expr, 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 |
| 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 |
| warnTacticDeprecation | Idris.Parser.Expr, Idris.Parser |
| warnTotality | Idris.Output |
| Warranty | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Watch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| weakenTm | Idris.Core.TT |
| WEnv | Idris.Core.WHNF |
| wExpr | Idris.Parser |
| WhatDocs | Idris.IdeMode |
| whereBlock | Idris.Parser |
| WhereN | Idris.Core.TT |
| while_elaborating | Idris.Core.ProofState, Idris.Core.Elaborate |
| whiteSpace | Idris.Parser.Helpers, Idris.Parser |
| WHNF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| whnf | Idris.Core.WHNF |
| WhoCalls | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| whoCalls | Idris.WhoCalls |
| withContext | Idris.AbsSyntax |
| withContext_ | Idris.AbsSyntax |
| withErrorReflection | Idris.Elab.Term |
| WithFnType | Idris.Core.TT |
| WithN | Idris.Core.TT |
| withTempdir | Util.System |
| WorldType | Idris.Core.TT |
| writeHighlights | Idris.Output |
| writeIBC | Idris.IBC |
| writePkgIndex | Idris.IBC |
| writeSource | Util.System |
| writeSourceText | Util.System |
| zipHere | Idris.Core.Elaborate |
| _fc_end | Idris.Core.TT |
| _fc_fname | Idris.Core.TT |
| _fc_start | Idris.Core.TT |