A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
#
$
%
&
+
.
/
<
=
>
?
@
\
^
|
-
_
All

Index - R

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