| R | |
| 1 (Data Constructor) | Agda.Auto.Options |
| 2 (Data Constructor) | Agda.Utils.Map |
| 3 (Type/Class) | Agda.TypeChecking.Serialise.Base |
| raise | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| raiseFrom | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| raiseS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| Range | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.Syntax.Position |
| 3 (Type/Class) | Agda.Interaction.Highlighting.Range |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Range |
| Range' | Agda.Syntax.Position |
| RangeAndPragma | |
| 1 (Type/Class) | Agda.Syntax.Translation.AbstractToConcrete |
| 2 (Data Constructor) | Agda.Syntax.Translation.AbstractToConcrete |
| Ranged | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| rangedThing | Agda.Syntax.Common |
| rangeFile | Agda.Syntax.Position |
| rangeIntervals | Agda.Syntax.Position |
| rangeInvariant | |
| 1 (Function) | Agda.Syntax.Position |
| 2 (Function) | Agda.Interaction.Highlighting.Range |
| rangeOf | Agda.Syntax.Common |
| Ranges | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Range |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Range |
| ranges | Agda.Interaction.Highlighting.Precise |
| rangesInvariant | Agda.Interaction.Highlighting.Range |
| rangesToPositions | Agda.Interaction.Highlighting.Range |
| rangeToEndPoints | Agda.Interaction.Highlighting.Range |
| rangeToInterval | Agda.Syntax.Position |
| rangeToIntervalWithFile | Agda.Syntax.Position |
| rangeToPositions | Agda.Interaction.Highlighting.Range |
| rational | Agda.Utils.Pretty |
| RawApp | Agda.Syntax.Concrete |
| RawAppP | Agda.Syntax.Concrete |
| RawName | Agda.Syntax.Common |
| rawNameToString | Agda.Syntax.Common |
| rawValue | Agda.Auto.Syntax |
| rbrace | Agda.Utils.Pretty |
| rbrack | Agda.Utils.Pretty |
| RConst | Agda.Utils.Warshall |
| reAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| ReachabilityProblem | Agda.Interaction.Highlighting.Precise |
| reachable | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| reachableFrom | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| readBinaryFile' | Agda.Utils.IO.Binary |
| ReadFileError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| readFromCachedLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| readInterface | Agda.Interaction.Imports |
| readIORef | Agda.Utils.IORef |
| readline | Agda.Interaction.Monad |
| readM | Agda.Utils.Monad |
| readModifyIORef' | Agda.Utils.IORef |
| ReadP | Agda.Utils.Parser.ReadP |
| readParse | Agda.Interaction.InteractionTop |
| readsToParse | Agda.Interaction.InteractionTop |
| ReadTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| readTextFile | Agda.Utils.IO.UTF8 |
| reallyFree | Agda.TypeChecking.Rewriting.NonLinMatch |
| ReallyNotBlocked | Agda.Syntax.Internal |
| reallyUnLevelView | Agda.TypeChecking.Level |
| rebindName | Agda.Syntax.Scope.Monad |
| Rec | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recalc | Agda.Auto.NarrowingSearch |
| recalcs | Agda.Auto.NarrowingSearch |
| reccalc | Agda.Auto.NarrowingSearch |
| RecCheck | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecDef | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| recEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recEtaEquality' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recNamedCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Recompile | |
| 1 (Type/Class) | Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Compiler.Backend |
| recomputeInScopeSets | Agda.Syntax.Scope.Base |
| recomputeInverseScopeMaps | Agda.Syntax.Scope.Base |
| reconstructParameters | Agda.TypeChecking.ReconstructParameters |
| reconstructParametersInEqView | Agda.TypeChecking.ReconstructParameters |
| reconstructParametersInTel | Agda.TypeChecking.ReconstructParameters |
| reconstructParametersInType | Agda.TypeChecking.ReconstructParameters |
| Record | |
| 1 (Type/Class) | Agda.Utils.Lens.Examples |
| 2 (Data Constructor) | Agda.Utils.Lens.Examples |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecordAssign | Agda.Syntax.Abstract |
| RecordAssignment | Agda.Syntax.Concrete |
| RecordAssignments | Agda.Syntax.Concrete |
| RecordAssigns | Agda.Syntax.Abstract |
| RecordCon | Agda.TypeChecking.Datatypes |
| RecordDef | Agda.Syntax.Reflected |
| recordFieldNames | Agda.TypeChecking.Records |
| RecordFlex | Agda.TypeChecking.Rules.LHS.Problem |
| recordModule | Agda.TypeChecking.Records |
| RecordModuleIFS | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recordPatternToProjections | Agda.TypeChecking.RecordPatterns |
| Records | Agda.TypeChecking.MetaVars |
| RecordSig | Agda.Syntax.Concrete |
| recoverAsPatterns | |
| 1 (Function) | Agda.Compiler.Treeless.AsPatterns |
| 2 (Function) | Agda.TypeChecking.Rules.LHS.AsPatterns |
| RecP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recRecursive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecSig | Agda.Syntax.Abstract |
| recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecUpdate | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recurseExpr | Agda.Syntax.Abstract.Views |
| recursive | Agda.Termination.RecCheck |
| recursiveRecord | Agda.TypeChecking.Records |
| RecursiveReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redBind | Agda.TypeChecking.Primitive |
| redEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redoChecks | Agda.Interaction.BasicOps |
| redReturn | Agda.TypeChecking.Primitive |
| redSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Reduce | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Type/Class) | Agda.TypeChecking.Reduce |
| reduce | Agda.TypeChecking.Reduce |
| reduce' | Agda.TypeChecking.Reduce |
| reduceB | Agda.TypeChecking.Reduce |
| reduceB' | Agda.TypeChecking.Reduce |
| Reduced | |
| 1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reduceDefCopy | Agda.TypeChecking.Reduce |
| ReduceEnv | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reduceHead | Agda.TypeChecking.Reduce |
| reduceHead' | Agda.TypeChecking.Reduce |
| ReduceM | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reduceProjectionLike | Agda.TypeChecking.ProjectionLike |
| reduceQuotedTerm | Agda.TypeChecking.Unquote |
| RefCreateEnv | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| Refinable | Agda.Auto.NarrowingSearch |
| Refine | Agda.Interaction.InteractionTop |
| refine | Agda.Interaction.BasicOps |
| Refinement | Agda.Auto.Auto |
| refinements | Agda.Auto.NarrowingSearch |
| refineMeta | Agda.Interaction.CommandLine |
| RefInfo | Agda.Auto.Syntax |
| reflClos | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Reflected | Agda.Syntax.Common |
| refreshStr | Agda.Interaction.InteractionTop |
| registerInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Reify | Agda.Syntax.Translation.InternalToAbstract |
| reify | Agda.Syntax.Translation.InternalToAbstract |
| reifyElimToExpr | Agda.Interaction.BasicOps |
| reifyPatterns | Agda.Syntax.Translation.InternalToAbstract |
| reifyWhen | Agda.Syntax.Translation.InternalToAbstract |
| Rel | Agda.TypeChecking.Primitive |
| Related | Agda.Syntax.Fixity |
| related | Agda.Utils.PartialOrd |
| RelativeTo | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Relevance | Agda.Syntax.Common |
| relevanceAction | Agda.TypeChecking.CheckInternal |
| RelevanceMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Relevant | Agda.Syntax.Common |
| relevantIn | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| relevantInIgnoringNonvariant | Agda.TypeChecking.Polarity |
| relevantInIgnoringSortAnn | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| relevantVars | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| relOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RelView | |
| 1 (Type/Class) | Agda.TypeChecking.Rewriting |
| 2 (Data Constructor) | Agda.TypeChecking.Rewriting |
| relView | Agda.TypeChecking.Rewriting |
| relViewCore | Agda.TypeChecking.Rewriting |
| relViewDelta | Agda.TypeChecking.Rewriting |
| relViewTel | Agda.TypeChecking.Rewriting |
| relViewType | Agda.TypeChecking.Rewriting |
| relViewType' | Agda.TypeChecking.Rewriting |
| removeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| removeNameFromScope | Agda.Syntax.Scope.Base |
| removeNode | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| removeOldInteractionScope | Agda.Interaction.InteractionTop |
| removeOnlyQualified | Agda.Syntax.Scope.Base |
| removePrivates | Agda.Interaction.Imports |
| removeSucs | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| removevar | Agda.Auto.CaseSplit |
| Ren | Agda.Syntax.Abstract |
| ren | Agda.Auto.CaseSplit |
| rename | Agda.Auto.Syntax |
| renameCanonicalNames | Agda.Syntax.Scope.Base |
| renameOffset | Agda.Auto.Syntax |
| renameP | Agda.TypeChecking.Substitute |
| Renaming | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Auto.Syntax |
| 3 (Type/Class) | Agda.Syntax.Concrete |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| renaming | Agda.TypeChecking.Substitute |
| Renaming' | Agda.Syntax.Common |
| renamingR | Agda.TypeChecking.Substitute |
| rEnd | Agda.Syntax.Position |
| rEnd' | Agda.Syntax.Position |
| render | Agda.Utils.Pretty |
| renderStyle | Agda.Utils.Pretty |
| renFrom | Agda.Syntax.Common |
| renModules | Agda.Syntax.Abstract |
| renNames | Agda.Syntax.Abstract |
| renTo | Agda.Syntax.Common |
| renToRange | Agda.Syntax.Common |
| reorder | Agda.Compiler.JS.Compiler |
| reorder' | Agda.Compiler.JS.Compiler |
| reorderTel | Agda.TypeChecking.Telescope |
| reorderTel_ | Agda.TypeChecking.Telescope |
| RepeatedVariablesInPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| repeatWhile | Agda.Utils.Function |
| repeatWhileM | Agda.Utils.Function |
| repl | Agda.Compiler.Common |
| Replace | Agda.Auto.CaseSplit |
| replace | Agda.Auto.CaseSplit |
| replace' | Agda.Auto.CaseSplit |
| replaceEmptyName | Agda.Syntax.Internal |
| replaceModuleExtension | Agda.Interaction.FindFile |
| replacep | Agda.Auto.CaseSplit |
| reportS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reportSDoc | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reportSLn | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ReqArg | Agda.Interaction.Options |
| requireLevels | Agda.TypeChecking.Level |
| requireOptionRewriting | Agda.TypeChecking.Rewriting |
| Res | Agda.TypeChecking.MetaVars |
| reset | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| resetAllState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| resetState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| resolvedLetBound | Agda.Syntax.Scope.Monad |
| ResolvedName | Agda.Syntax.Scope.Monad |
| resolvedVar | Agda.Syntax.Scope.Monad |
| resolveModule | Agda.Syntax.Scope.Monad |
| resolveName | Agda.Syntax.Scope.Monad |
| resolveName' | Agda.Syntax.Scope.Monad |
| resolveUnknownInstanceDefs | Agda.TypeChecking.Telescope |
| RespectFlags | Agda.Interaction.Options |
| Response | Agda.Interaction.Response |
| response | Agda.Interaction.EmacsCommand |
| Resp_ClearHighlighting | Agda.Interaction.Response |
| Resp_ClearRunningInfo | Agda.Interaction.Response |
| Resp_DisplayInfo | Agda.Interaction.Response |
| Resp_DoneAborting | Agda.Interaction.Response |
| Resp_GiveAction | Agda.Interaction.Response |
| Resp_HighlightingInfo | Agda.Interaction.Response |
| Resp_InteractionPoints | Agda.Interaction.Response |
| Resp_JumpToError | Agda.Interaction.Response |
| Resp_MakeCase | Agda.Interaction.Response |
| Resp_RunningInfo | Agda.Interaction.Response |
| Resp_SolveAll | Agda.Interaction.Response |
| Resp_Status | Agda.Interaction.Response |
| Restore | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| restorePostScopeState | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| restPats | Agda.TypeChecking.Rules.LHS.Problem |
| restrictLocalPrivate | Agda.Syntax.Scope.Base |
| restrictPrivate | Agda.Syntax.Scope.Base |
| restType | Agda.TypeChecking.Rules.LHS.Problem |
| Result | Agda.Termination.TermCheck |
| retryConstraints | Agda.Interaction.CommandLine |
| Return | Agda.Interaction.CommandLine |
| returnTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reverseP | Agda.Utils.Permutation |
| revisitRecordPatternTranslation | Agda.TypeChecking.Rules.Decl |
| revLift | Agda.Interaction.InteractionTop |
| rewArity | Agda.TypeChecking.Rewriting |
| rewContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rewHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rewName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rewPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rewRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Rewrite | Agda.Interaction.BasicOps |
| rewrite | Agda.TypeChecking.Rewriting |
| RewriteEqn | Agda.Syntax.Concrete |
| rewriteExprs | Agda.Syntax.Abstract |
| RewritePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| RewriteRHS | Agda.Syntax.Abstract |
| rewriteRHS | Agda.Syntax.Abstract |
| RewriteRule | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RewriteRuleMap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rewriteWhereDecls | Agda.Syntax.Abstract |
| rewriteWith | Agda.TypeChecking.Rewriting |
| rewType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RHS | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| Rhs | Agda.Utils.Haskell.Syntax |
| RHS' | Agda.Syntax.Concrete |
| rhsConcrete | Agda.Syntax.Abstract |
| rhsExpr | Agda.Syntax.Abstract |
| ribbonsPerLine | Agda.Utils.Pretty |
| RICheckElim | Agda.Auto.Syntax |
| RICheckProjIndex | Agda.Auto.Syntax |
| RICopyInfo | Agda.Auto.Syntax |
| rieDefFreeVars | Agda.Auto.Syntax |
| rieEqReasoningConsts | Agda.Auto.Syntax |
| rieHints | Agda.Auto.Syntax |
| RIEnv | Agda.Auto.Syntax |
| RIEqRState | Agda.Auto.Syntax |
| RightAssoc | Agda.Syntax.Fixity |
| RightDisjunct | Agda.Auto.NarrowingSearch |
| rightExpr | Agda.TypeChecking.SizedTypes.Syntax |
| RightHandSide | Agda.Syntax.Translation.ConcreteToAbstract |
| rightMargin | Agda.Syntax.Position |
| RightOperandCtx | Agda.Syntax.Fixity |
| Rigid | |
| 1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 3 (Type/Class) | Agda.Utils.Warshall |
| 4 (Data Constructor) | Agda.Utils.Warshall |
| 5 (Data Constructor) | Agda.TypeChecking.SizedTypes |
| 6 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| rigid | Agda.TypeChecking.SizedTypes.Syntax |
| RigidId | |
| 1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Utils.Warshall |
| rigidId | Agda.TypeChecking.SizedTypes.Syntax |
| rigidIndex | Agda.TypeChecking.SizedTypes.Solve |
| rigidlyConstrainedMetas | Agda.TypeChecking.InstanceArguments |
| rigidName | Agda.TypeChecking.SizedTypes.Solve |
| Rigids | Agda.TypeChecking.SizedTypes.Syntax |
| rigids | Agda.TypeChecking.SizedTypes.Syntax |
| rigidVars | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| rigidVarsNotContainedIn | Agda.TypeChecking.MetaVars.Occurs |
| RIInferredTypeUnknown | Agda.Auto.Syntax |
| RIIotaStep | Agda.Auto.Syntax |
| riMainCxtLength | Agda.Auto.Syntax |
| RIMainInfo | Agda.Auto.Syntax |
| riMainIota | Agda.Auto.Syntax |
| riMainType | Agda.Auto.Syntax |
| RINotConstructor | Agda.Auto.Syntax |
| RIPickSubsvar | Agda.Auto.Syntax |
| RIUnifInfo | Agda.Auto.Syntax |
| RIUsedVars | Agda.Auto.Syntax |
| rm | Agda.Auto.NarrowingSearch |
| rollback | Agda.Syntax.Parser.LookAhead |
| rootNameModule | Agda.Interaction.FindFile |
| rootPath | Agda.Utils.FileName |
| roundFixBrackets | Agda.Syntax.Fixity |
| row | Agda.Termination.SparseMatrix |
| rowdescr | Agda.Utils.Warshall |
| rows | Agda.Termination.SparseMatrix |
| rparen | Agda.Utils.Pretty |
| rStart | Agda.Syntax.Position |
| rStart' | Agda.Syntax.Position |
| RString | Agda.Syntax.Common |
| rtmError | Agda.Compiler.MAlonzo.Misc |
| rtmIncompleteMatch | Agda.Compiler.MAlonzo.Misc |
| rtmQual | Agda.Compiler.MAlonzo.Misc |
| rtmUnreachableError | Agda.Compiler.MAlonzo.Misc |
| rtmVar | Agda.Compiler.MAlonzo.Misc |
| rToR | Agda.Interaction.Highlighting.Range |
| rtrim | Agda.Utils.String |
| runAbsToCon | Agda.Syntax.Translation.AbstractToConcrete |
| runAgda | Agda.Main |
| runAgda' | Agda.Main |
| runAgdaWithOptions | Agda.Main |
| runChange | Agda.Utils.Update |
| runExceptT | Agda.Utils.Except |
| runFree | Agda.TypeChecking.Free |
| runFreeM | Agda.TypeChecking.Free.Lazy |
| runGetState | Agda.TypeChecking.Serialise.Base |
| runIM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad, Agda.Compiler.Backend |
| runInteraction | Agda.Interaction.InteractionTop |
| runListT | Agda.Utils.ListT |
| runLookAhead | Agda.Syntax.Parser.LookAhead |
| RunMetaOccursCheck | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runMListT | Agda.Utils.ListT |
| runNice | Agda.Syntax.Concrete.Definitions |
| runNLM | Agda.TypeChecking.Rewriting.NonLinMatch |
| runOptM | Agda.Interaction.Options |
| runPM | Agda.TypeChecking.Warnings |
| runPMIO | Agda.Syntax.Parser |
| runReduceF | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runRefCreateEnv | Agda.Auto.NarrowingSearch |
| runSafeTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runTCMPrettyErrors | Agda.Main |
| runTCMTop | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runTCMTop' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runTer | Agda.Termination.Monad |
| runTerDefault | Agda.Termination.Monad |
| runUndo | Agda.Auto.NarrowingSearch |
| runUnquoteM | Agda.TypeChecking.Unquote |
| runUpdater | Agda.Utils.Update |
| RVar | Agda.Utils.Warshall |