| R | Agda.TypeChecking.Serialise.Base |
| raise | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| raiseErrors | Agda.Interaction.Library.Base |
| raiseErrors' | Agda.Interaction.Library.Base |
| raiseExeNotExecutable | Agda.TypeChecking.Unquote |
| raiseExeNotFound | Agda.TypeChecking.Unquote |
| raiseExeNotTrusted | Agda.TypeChecking.Unquote |
| raiseFrom | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| raiseFromS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| raiseS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| raiseWarningsOnUsage | Agda.TypeChecking.Warnings |
| 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.Utils.IArray |
| 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 | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.Syntax.Position |
| rangeFile | Agda.Syntax.Position |
| rangeFileName | Agda.Syntax.Position |
| rangeFilePath | Agda.Syntax.Position |
| rangeIntervals | Agda.Syntax.Position |
| rangeInvariant | |
| 1 (Function) | Agda.Syntax.Position |
| 2 (Function) | Agda.Interaction.Highlighting.Range |
| RangeMap | |
| 1 (Type/Class) | Agda.Utils.RangeMap |
| 2 (Data Constructor) | Agda.Utils.RangeMap |
| rangeMap | Agda.Utils.RangeMap |
| rangeMapInvariant | Agda.Utils.RangeMap |
| rangeModule | Agda.Syntax.Position |
| rangeModule' | Agda.Syntax.Position |
| rangeOf | Agda.Syntax.Common |
| RangePair | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| rangePair | Agda.Interaction.Highlighting.Precise |
| rangePairInvariant | Agda.Interaction.Highlighting.Precise |
| Ranges | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Range |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Range |
| rangesInvariant | Agda.Interaction.Highlighting.Range |
| rangeSize | Agda.Utils.IArray |
| rangesToPositions | Agda.Interaction.Highlighting.Range |
| rangeToInterval | Agda.Syntax.Position |
| rangeToIntervalWithFile | Agda.Syntax.Position |
| rangeToPositions | Agda.Interaction.Highlighting.Range |
| rangeToRange | Agda.Interaction.Highlighting.Range |
| rational | Agda.Syntax.Common.Pretty |
| ratioToDouble | Agda.Utils.Float |
| RawApp | Agda.Syntax.Concrete |
| rawApp | Agda.Syntax.Concrete |
| RawAppP | Agda.Syntax.Concrete |
| rawAppP | Agda.Syntax.Concrete |
| rawModuleNameParts | Agda.Syntax.TopLevelModuleName |
| rawModuleNameRange | Agda.Syntax.TopLevelModuleName |
| RawName | Agda.Syntax.Common |
| rawNameToString | Agda.Syntax.Common |
| RawTopLevelModuleName | |
| 1 (Type/Class) | Agda.Syntax.TopLevelModuleName |
| 2 (Data Constructor) | Agda.Syntax.TopLevelModuleName |
| rawTopLevelModuleName | Agda.Syntax.TopLevelModuleName |
| rawTopLevelModuleNameForModule | Agda.Syntax.TopLevelModuleName |
| rawTopLevelModuleNameForModuleName | Agda.Syntax.TopLevelModuleName |
| rawTopLevelModuleNameForQName | Agda.Syntax.TopLevelModuleName |
| rawTopLevelModuleNameToString | Agda.Syntax.TopLevelModuleName |
| rbrace | Agda.Syntax.Common.Pretty |
| rbrack | Agda.Syntax.Common.Pretty |
| RConst | Agda.Utils.Warshall |
| reAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| reachable | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| reachableFrom | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| reachableFromSet | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| readBinaryFile' | Agda.Utils.IO.Binary |
| ReadError | Agda.Interaction.Library.Base |
| ReadException | Agda.Utils.IO.UTF8 |
| ReadFailure | Agda.Interaction.Library.Base |
| readFile | Agda.Utils.IO.UTF8 |
| ReadFileError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| readFilePM | Agda.Syntax.Parser |
| readFromCachedLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ReadGHCModuleEnv | Agda.Compiler.MAlonzo.Misc |
| readInterface | Agda.Interaction.Imports |
| readIORef | Agda.Utils.IORef |
| readline | Agda.Interaction.Monad |
| readModifyIORef' | Agda.Utils.IORef |
| readParse | Agda.Interaction.Base |
| readsToParse | Agda.Interaction.Base |
| ReadTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| readTextFile | Agda.Utils.IO.UTF8 |
| readTokens | Agda.Mimer.Options |
| reallyAllReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ReallyDontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reallyDontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reallyFree | Agda.TypeChecking.Free.Reduce |
| reallyNoConstraints | Agda.TypeChecking.Constraints |
| ReallyNotBlocked | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| reallyNotFreeIn | Agda.TypeChecking.MetaVars.Occurs |
| 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 |
| RecCheck | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recComp | 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 |
| recConstructor | Agda.Syntax.Common |
| RecDef | Agda.Syntax.Abstract |
| RecDefS | Agda.Syntax.Abstract |
| 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 |
| recHasEta | Agda.Syntax.Common |
| recheckAbstractClause | Agda.Interaction.MakeCase |
| recheckBecausePragmaOptionsChanged | Agda.Interaction.Options |
| recInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recInductive | Agda.Syntax.Common |
| recMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecName | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base |
| recNamedCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Recompile | |
| 1 (Type/Class) | Agda.Compiler.Backend.Base, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Compiler.Backend.Base, Agda.Compiler.Backend |
| recomputeInScopeSets | Agda.Syntax.Scope.Base |
| recomputeInverseScopeMaps | Agda.Syntax.Scope.Base |
| reconstruct | Agda.TypeChecking.ReconstructParameters |
| reconstructAction | Agda.TypeChecking.ReconstructParameters |
| reconstructAction' | Agda.TypeChecking.ReconstructParameters |
| reconstructParameters | Agda.TypeChecking.ReconstructParameters |
| reconstructParameters' | Agda.TypeChecking.ReconstructParameters |
| reconstructParametersInEqView | Agda.TypeChecking.ReconstructParameters |
| reconstructParametersInTel | Agda.TypeChecking.ReconstructParameters |
| reconstructParametersInType | 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.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| 4 (Data Constructor) | Agda.Syntax.Concrete |
| 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 |
| RecordData | |
| 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 |
| RecordDef | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| RecordDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecordDirective | Agda.Syntax.Concrete |
| RecordDirectives | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| RecordDirectives' | Agda.Syntax.Common |
| recordEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recordFieldNames | Agda.TypeChecking.Records |
| RecordFieldWarning | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recordFieldWarningToError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecordFlex | Agda.TypeChecking.Rules.LHS.Problem |
| recordInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecordModuleInstance | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recordPatternToProjections | Agda.TypeChecking.RecordPatterns |
| recordRHSToCopatterns | Agda.TypeChecking.RecordPatterns |
| Records | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecordSig | Agda.Syntax.Concrete |
| recoverAsPatterns | Agda.Compiler.Treeless.AsPatterns |
| recoverLayout | Agda.Syntax.Parser.Helpers |
| RecP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recPattern | Agda.Syntax.Common |
| recPatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recRecursive | 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 |
| RecSigS | Agda.Syntax.Abstract |
| recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| recTerminates | 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 |
| RecurseExprFn | Agda.Syntax.Abstract.Views |
| RecurseExprRecFn | Agda.Syntax.Abstract.Views |
| recursive | Agda.Termination.RecCheck |
| recursiveRecord | Agda.TypeChecking.Records |
| RecursiveRecordNeedsInductivity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RecursiveReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redBind | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redoChecks | Agda.Interaction.BasicOps |
| redPred | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redReturn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| redReturnNoSimpl | Agda.TypeChecking.Primitive.Cubical, 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 |
| reduce2Lam | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| reduceAllDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ReduceAndEtaContract | Agda.TypeChecking.MetaVars |
| reduceAndEtaContract | Agda.TypeChecking.MetaVars |
| 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 |
| reduceDefCopyTCM | Agda.TypeChecking.Reduce |
| ReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| reduceEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reduceHead | Agda.TypeChecking.Reduce |
| reduceIApply' | 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 |
| reduceSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reduceWithBlocker | Agda.TypeChecking.Reduce |
| ReferencesFutureVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Refine | Agda.Interaction.InteractionTop |
| refine | Agda.Interaction.BasicOps |
| reflClos | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Reflected | Agda.Syntax.Common |
| Reflection | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| registerInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ReifiesTo | Agda.Syntax.Translation.InternalToAbstract |
| Reify | Agda.Syntax.Translation.InternalToAbstract |
| reify | Agda.Syntax.Translation.InternalToAbstract |
| reifyDisplayFormP | Agda.Syntax.Translation.InternalToAbstract |
| reifyElimToExpr | Agda.Interaction.BasicOps |
| reifyPatterns | Agda.Syntax.Translation.InternalToAbstract |
| reifyUnblocked | Agda.Syntax.Translation.InternalToAbstract |
| reifyWhen | Agda.Syntax.Translation.InternalToAbstract |
| reintroduceEllipsis | Agda.Syntax.Concrete.Pattern |
| rejectUnknownFields | Agda.Interaction.JSON |
| Rel | Agda.TypeChecking.Primitive |
| Related | Agda.Syntax.Common |
| related | Agda.Utils.PartialOrd |
| relativizeAbsolutePath | Agda.Utils.FileName |
| Relevance | Agda.Syntax.Common |
| RelevanceAttribute | Agda.Syntax.Concrete.Attribute |
| relevanceAttributes | Agda.Syntax.Concrete.Attribute |
| relevanceAttributeTable | Agda.Syntax.Concrete.Attribute |
| RelevanceMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Relevant | Agda.Syntax.Common |
| relevantIn | Agda.TypeChecking.Free |
| relevantInIgnoringSortAnn | Agda.TypeChecking.Free |
| relOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| relToDontCare | Agda.TypeChecking.Substitute |
| 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 |
| RemoteMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RemoteMetaVariable | |
| 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 |
| Remove | |
| 1 (Type/Class) | Agda.Interaction.Base |
| 2 (Data Constructor) | Agda.Interaction.Base |
| removeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| RemoveHighlighting | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| removeLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| removeLetBindingsFrom | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| removeLoneSig | Agda.Syntax.Concrete.Definitions.Monad |
| removeNameFromScope | Agda.Syntax.Scope.Base |
| removeNode | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| removeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| removeOldInteractionScope | Agda.Interaction.InteractionTop |
| removeParenP | Agda.Syntax.Concrete |
| removeSucs | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RemoveTokenBasedHighlighting | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Ren | Agda.Syntax.Abstract |
| renameCanonicalNames | Agda.Syntax.Scope.Base |
| renameNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| renameNodesMonotonic | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| renameP | Agda.TypeChecking.Substitute |
| renameTel | Agda.TypeChecking.Telescope |
| Renaming | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| renaming | Agda.TypeChecking.Substitute |
| Renaming' | Agda.Syntax.Common |
| RenamingDirective | Agda.Syntax.Concrete |
| RenamingDirective' | Agda.Syntax.Common |
| renamingR | Agda.TypeChecking.Substitute |
| rEnd | Agda.Syntax.Position |
| rEnd' | Agda.Syntax.Position |
| render | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| renderAnsiIO | Agda.Syntax.Common.Pretty.ANSI |
| renderError | Agda.TypeChecking.Errors |
| renderErrorParts | Agda.TypeChecking.Unquote |
| renderSpans | Agda.Syntax.Common.Pretty |
| renderStyle | Agda.Syntax.Common.Pretty |
| renderSuffix | Agda.Utils.Suffix |
| renFixity | Agda.Syntax.Common |
| 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 |
| repeat | Agda.Utils.List1 |
| RepeatedVariablesInPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| repeatWhile | Agda.Utils.Function |
| repeatWhileM | Agda.Utils.Function |
| repl | |
| 1 (Function) | Agda.Compiler.Common |
| 2 (Function) | Agda.Interaction.AgdaTop |
| replaceEmptyName | Agda.Syntax.Internal |
| replacementChar | Agda.Utils.Char |
| replaceModuleExtension | Agda.Interaction.FindFile |
| replaceSurrogateCodePoint | Agda.Utils.Char |
| replInteractor | Agda.Main |
| reportResult | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ReportS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| requireAllowExec | Agda.TypeChecking.Unquote |
| requireCubical | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| requireLevels | Agda.TypeChecking.Level |
| requireOptionRewriting | Agda.TypeChecking.Rewriting |
| RequiresDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Res | Agda.TypeChecking.MetaVars |
| reset | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| resetAllState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| resetLayoutStatus | Agda.Syntax.Parser.Monad |
| resetState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| resolvedBindingSource | Agda.Syntax.Scope.Base |
| ResolvedName | Agda.Syntax.Scope.Base |
| resolvedVar | Agda.Syntax.Scope.Base |
| ResolveInstanceHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| resolveInstanceHead | Agda.TypeChecking.InstanceArguments |
| ResolveInstanceOF | Agda.Interaction.Base |
| resolveModule | Agda.Syntax.Scope.Monad |
| resolveName | Agda.Syntax.Scope.Monad |
| resolveName' | Agda.Syntax.Scope.Monad |
| respInScope | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| respLetValue | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Response | Agda.Interaction.Response |
| response | Agda.Interaction.EmacsCommand |
| ResponseContextEntry | |
| 1 (Type/Class) | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| 2 (Data Constructor) | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Response_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| respOrigName | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| respReifName | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| respType | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_ClearHighlighting | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_ClearRunningInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_DisplayInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_DoneAborting | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_DoneExiting | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_GiveAction | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_HighlightingInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_InteractionPoints | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_JumpToError | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_MakeCase | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_Mimer | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_RunningInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_SolveAll | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Resp_Status | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| restorePostScopeState | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| restrictLocalPrivate | Agda.Syntax.Scope.Base |
| restrictPrivate | Agda.Syntax.Scope.Base |
| restrictTo | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| Result | Agda.Termination.TermCheck |
| resultBlocker | Agda.TypeChecking.DiscrimTree |
| resultValues | Agda.TypeChecking.DiscrimTree |
| Retract | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
| returnExpr | Agda.Syntax.Concrete |
| returnTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| reverse | Agda.Utils.List1 |
| ReversedSuffix | Agda.Utils.List |
| reverseP | Agda.Utils.Permutation |
| revisitRecordPatternTranslation | Agda.TypeChecking.Rules.Decl |
| revLift | Agda.Interaction.InteractionTop |
| revLiftTC | Agda.Interaction.InteractionTop |
| rewContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rewFromClause | 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 | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Interaction.Base |
| rewrite | Agda.TypeChecking.Rewriting |
| RewriteAmbiguousRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RewriteAmbiguousRules_ | Agda.Interaction.Options.Warnings |
| RewriteBeforeFunctionDefinition_ | Agda.Interaction.Options.Warnings |
| RewriteBeforeMutualFunctionDefinition_ | Agda.Interaction.Options.Warnings |
| RewriteBlockedOnProblems_ | Agda.Interaction.Options.Warnings |
| RewriteConstructorParametersNotGeneral_ | Agda.Interaction.Options.Warnings |
| RewriteContainsUnsolvedMetaVariables_ | Agda.Interaction.Options.Warnings |
| RewriteDoesNotTargetRewriteRelation_ | Agda.Interaction.Options.Warnings |
| RewriteEqn | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| RewriteEqn' | Agda.Syntax.Common |
| rewriteExprs | Agda.Syntax.Abstract |
| RewriteHeadSymbolContainsMetas_ | Agda.Interaction.Options.Warnings |
| RewriteHeadSymbolIsProjectionLikeFunction_ | Agda.Interaction.Options.Warnings |
| RewriteHeadSymbolIsProjection_ | Agda.Interaction.Options.Warnings |
| RewriteHeadSymbolIsTypeConstructor_ | Agda.Interaction.Options.Warnings |
| RewriteLHSNotDefinitionOrConstructor_ | Agda.Interaction.Options.Warnings |
| RewriteLHSReduces_ | Agda.Interaction.Options.Warnings |
| RewriteMaybeNonConfluent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RewriteMaybeNonConfluent_ | Agda.Interaction.Options.Warnings |
| RewriteMissingRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RewriteMissingRule_ | Agda.Interaction.Options.Warnings |
| RewriteNonConfluent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| RewriteNonConfluent_ | Agda.Interaction.Options.Warnings |
| RewritePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| rewriteRelationDom | Agda.TypeChecking.Rewriting |
| RewriteRequiresDefinitions_ | Agda.Interaction.Options.Warnings |
| RewriteRHS | Agda.Syntax.Abstract |
| rewriteRHS | Agda.Syntax.Abstract |
| RewriteRHSS | 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 |
| rewriteStrippedPats | Agda.Syntax.Abstract |
| RewriteVariablesBoundMoreThanOnce_ | Agda.Interaction.Options.Warnings |
| RewriteVariablesNotBoundByLHS_ | Agda.Interaction.Options.Warnings |
| 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 |
| RHSOrTypeSigs | Agda.Syntax.Parser.Helpers |
| RHSS | Agda.Syntax.Abstract |
| RHSSpine | Agda.Syntax.Abstract |
| rhsSpine | Agda.Syntax.Abstract |
| ribbonsPerLine | Agda.Syntax.Common.Pretty |
| RightAssoc | Agda.Syntax.Common |
| rightExpr | Agda.TypeChecking.SizedTypes.Syntax |
| rightIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
| rightMargin | Agda.Syntax.Position |
| RightOperandCtx | Agda.Syntax.Fixity |
| rights | Agda.Utils.List1 |
| 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 |
| 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.Syntax |
| RigidK | Agda.TypeChecking.DiscrimTree.Types |
| rigidName | Agda.TypeChecking.SizedTypes.Syntax |
| RigidOf | Agda.TypeChecking.SizedTypes.Syntax |
| Rigids | Agda.TypeChecking.SizedTypes.Syntax |
| rigids | Agda.TypeChecking.SizedTypes.Syntax |
| rigidVars | Agda.TypeChecking.Free |
| rigidVarsNotContainedIn | Agda.TypeChecking.MetaVars.Occurs |
| RLiteral | Agda.Syntax.Literal |
| rmvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rmvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rmvModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rollback | Agda.Syntax.Parser.LookAhead |
| RollBackMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| rootNameModule | Agda.Interaction.FindFile |
| RootNameModuleNotAQualifiedModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| roundFixBrackets | Agda.Syntax.Fixity |
| row | Agda.Termination.SparseMatrix |
| rowdescr | Agda.Utils.Warshall |
| rows | Agda.Termination.SparseMatrix |
| rparen | Agda.Syntax.Common.Pretty |
| rStart | Agda.Syntax.Position |
| rStart' | Agda.Syntax.Position |
| RstFileType | Agda.Syntax.Common |
| RString | Agda.Syntax.Common |
| rtmError | Agda.Compiler.MAlonzo.Misc |
| rtmHole | 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 |
| runBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runBuiltinAccess | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runChange | Agda.Utils.Update |
| runChangeT | Agda.Utils.Update |
| runFail | Agda.Utils.Fail |
| runFail_ | Agda.Utils.Fail |
| runFree | Agda.TypeChecking.Free |
| runFreeM | Agda.TypeChecking.Free.Lazy |
| runGetState | Agda.TypeChecking.Serialise.Base |
| runHighlighter | Agda.Interaction.Highlighting.FromAbstract |
| runHsCompileT | Agda.Compiler.MAlonzo.Misc |
| runHsCompileT' | Agda.Compiler.MAlonzo.Misc |
| runIM | Agda.Interaction.Monad |
| runInteraction | Agda.Interaction.InteractionTop |
| runInteractionLoop | Agda.Interaction.CommandLine |
| runLexAction | Agda.Syntax.Parser.Alex |
| 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 |
| runNames | Agda.TypeChecking.Names |
| runNamesT | Agda.TypeChecking.Names |
| runNice | Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions |
| runNLM | Agda.TypeChecking.Rewriting.NonLinMatch |
| runOptM | Agda.Interaction.Options |
| runP | Agda.Interaction.Library.Parse |
| runPM | Agda.TypeChecking.Warnings |
| runPMIO | Agda.Syntax.Parser |
| runPureConversion | Agda.TypeChecking.Conversion.Pure |
| RunRecordPatternTranslation | |
| 1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile |
| 2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile |
| runReduceF | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runSafeTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| runStConcreteNames | 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 |
| runUnifyLogT | Agda.TypeChecking.Rules.LHS.Unify.Types |
| runUnquoteM | Agda.TypeChecking.Unquote |
| runUpdater | Agda.Utils.Update |
| runUpdaterT | Agda.Utils.Update |
| RVar | Agda.Utils.Warshall |