Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant

Index - R

R 
1 (Data Constructor)Agda.Auto.Options
2 (Type/Class)Agda.TypeChecking.Serialise.Base
raiseAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseErrorsAgda.Interaction.Library.Base
raiseErrors'Agda.Interaction.Library.Base
raiseExeNotExecutableAgda.TypeChecking.Unquote
raiseExeNotFoundAgda.TypeChecking.Unquote
raiseExeNotTrustedAgda.TypeChecking.Unquote
raiseFromAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseFromSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseWarningsOnUsageAgda.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.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
rangedThingAgda.Syntax.Common
RangeFile 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
rangeFileAgda.Syntax.Position
rangeFileNameAgda.Syntax.Position
rangeFilePathAgda.Syntax.Position
rangeIntervalsAgda.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
rangeMapAgda.Utils.RangeMap
rangeMapInvariantAgda.Utils.RangeMap
rangeModuleAgda.Syntax.Position
rangeModule'Agda.Syntax.Position
rangeOfAgda.Syntax.Common
RangePair 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
rangePairAgda.Interaction.Highlighting.Precise
rangePairInvariantAgda.Interaction.Highlighting.Precise
Ranges 
1 (Type/Class)Agda.Interaction.Highlighting.Range
2 (Data Constructor)Agda.Interaction.Highlighting.Range
rangesInvariantAgda.Interaction.Highlighting.Range
rangesToPositionsAgda.Interaction.Highlighting.Range
rangeToIntervalAgda.Syntax.Position
rangeToIntervalWithFileAgda.Syntax.Position
rangeToPositionsAgda.Interaction.Highlighting.Range
rangeToRangeAgda.Interaction.Highlighting.Range
rationalAgda.Utils.Pretty
ratioToDoubleAgda.Utils.Float
RawAppAgda.Syntax.Concrete
rawAppAgda.Syntax.Concrete
RawAppPAgda.Syntax.Concrete
rawAppPAgda.Syntax.Concrete
rawModuleNamePartsAgda.Syntax.TopLevelModuleName
rawModuleNameRangeAgda.Syntax.TopLevelModuleName
RawNameAgda.Syntax.Common
rawNameToStringAgda.Syntax.Common
RawTopLevelModuleName 
1 (Type/Class)Agda.Syntax.TopLevelModuleName
2 (Data Constructor)Agda.Syntax.TopLevelModuleName
rawTopLevelModuleNameAgda.Syntax.TopLevelModuleName
rawTopLevelModuleNameForModuleAgda.Syntax.TopLevelModuleName
rawTopLevelModuleNameForModuleNameAgda.Syntax.TopLevelModuleName
rawTopLevelModuleNameForQNameAgda.Syntax.TopLevelModuleName
rawTopLevelModuleNameToStringAgda.Syntax.TopLevelModuleName
rawValueAgda.Auto.Syntax
rbraceAgda.Utils.Pretty
rbrackAgda.Utils.Pretty
RConstAgda.Utils.Warshall
reAbsAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
reachableAgda.Utils.Graph.AdjacencyMap.Unidirectional
reachableFromAgda.Utils.Graph.AdjacencyMap.Unidirectional
reachableFromSetAgda.Utils.Graph.AdjacencyMap.Unidirectional
readBinaryFile'Agda.Utils.IO.Binary
ReadErrorAgda.Interaction.Library.Base
ReadExceptionAgda.Utils.IO.UTF8
ReadFailureAgda.Interaction.Library.Base
readFileAgda.Utils.IO.UTF8
ReadFileErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
readFilePMAgda.Syntax.Parser
readFromCachedLogAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
ReadGHCModuleEnvAgda.Compiler.MAlonzo.Misc
ReadGHCOptsAgda.Compiler.MAlonzo.Compiler
readInterfaceAgda.Interaction.Imports
readIORefAgda.Utils.IORef
readlineAgda.Interaction.Monad
readModifyIORef'Agda.Utils.IORef
readParseAgda.Interaction.Base
readsToParseAgda.Interaction.Base
ReadTCStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
readTextFileAgda.Utils.IO.UTF8
reallyAllReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReallyDontExpandLastAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reallyDontExpandLastAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
reallyFreeAgda.TypeChecking.Free.Reduce
ReallyNotBlockedAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
reallyNotFreeInAgda.TypeChecking.MetaVars.Occurs
reallyUnLevelViewAgda.TypeChecking.Level
rebindNameAgda.Syntax.Scope.Monad
Rec 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recAbstrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recalcAgda.Auto.NarrowingSearch
recalcsAgda.Auto.NarrowingSearch
reccalcAgda.Auto.NarrowingSearch
RecCheckAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
recClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recCompAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recConAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recConHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recConstructorAgda.Syntax.Common
RecDefAgda.Syntax.Abstract
RecDefSAgda.Syntax.Abstract
recEtaEqualityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recEtaEquality'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recFieldsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recHasEtaAgda.Syntax.Common
recheckAbstractClauseAgda.Interaction.MakeCase
recheckBecausePragmaOptionsChangedAgda.Interaction.Options
recInductionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recInductiveAgda.Syntax.Common
recMutualAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecName 
1 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor)Agda.Syntax.Scope.Base
recNamedConAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Recompile 
1 (Type/Class)Agda.Compiler.Backend
2 (Data Constructor)Agda.Compiler.Backend
recomputeInScopeSetsAgda.Syntax.Scope.Base
recomputeInverseScopeMapsAgda.Syntax.Scope.Base
reconstructAgda.TypeChecking.ReconstructParameters
reconstructActionAgda.TypeChecking.ReconstructParameters
reconstructAction'Agda.TypeChecking.ReconstructParameters
reconstructParametersAgda.TypeChecking.ReconstructParameters
reconstructParameters'Agda.TypeChecking.ReconstructParameters
reconstructParametersInEqViewAgda.TypeChecking.ReconstructParameters
reconstructParametersInTelAgda.TypeChecking.ReconstructParameters
reconstructParametersInTypeAgda.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.Compiler.Backend, Agda.TypeChecking.Monad
RecordAssignAgda.Syntax.Abstract
RecordAssignmentAgda.Syntax.Concrete
RecordAssignmentsAgda.Syntax.Concrete
RecordAssignsAgda.Syntax.Abstract
RecordConAgda.TypeChecking.Datatypes
RecordData 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecordDef 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Reflected
RecordDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecordDirective 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)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
recordEtaEqualityAgda.TypeChecking.Rules.LHS
recordFieldNamesAgda.TypeChecking.Records
RecordFieldWarning 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recordFieldWarningToErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecordFlexAgda.TypeChecking.Rules.LHS.Problem
recordInductionAgda.TypeChecking.Rules.LHS
RecordModuleInstance 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recordPatternToProjectionsAgda.TypeChecking.RecordPatterns
RecordsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
RecordSigAgda.Syntax.Concrete
recoverAsPatternsAgda.Compiler.Treeless.AsPatterns
RecP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recParsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recPatternAgda.Syntax.Common
recPatternMatchingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recRecursiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecSigAgda.Syntax.Abstract
RecSigSAgda.Syntax.Abstract
recTelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recTerminatesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecUpdate 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recurseExprAgda.Syntax.Abstract.Views
RecurseExprFnAgda.Syntax.Abstract.Views
RecurseExprRecFnAgda.Syntax.Abstract.Views
recursiveAgda.Termination.RecCheck
recursiveRecordAgda.TypeChecking.Records
RecursiveReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redBindAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redoChecksAgda.Interaction.BasicOps
redPredAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redReturnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redReturnNoSimplAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
redStAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Reduce 
1 (Data Constructor)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class)Agda.TypeChecking.Reduce
reduceAgda.TypeChecking.Reduce
reduce'Agda.TypeChecking.Reduce
reduce2LamAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
reduceAllDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReduceAndEtaContractAgda.TypeChecking.MetaVars
reduceAndEtaContractAgda.TypeChecking.MetaVars
reduceBAgda.TypeChecking.Reduce
reduceB'Agda.TypeChecking.Reduce
Reduced 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceDefCopyAgda.TypeChecking.Reduce
reduceDefCopyTCMAgda.TypeChecking.Reduce
ReduceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReduceEnv 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceHeadAgda.TypeChecking.Reduce
reduceIApply'Agda.TypeChecking.Reduce
ReduceM 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceProjectionLikeAgda.TypeChecking.ProjectionLike
reduceQuotedTermAgda.TypeChecking.Unquote
reduceStAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceWithBlockerAgda.TypeChecking.Reduce
RefCreateEnv 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
RefinableAgda.Auto.NarrowingSearch
RefineAgda.Interaction.InteractionTop
refineAgda.Interaction.BasicOps
RefinementAgda.Auto.Auto
refinementsAgda.Auto.NarrowingSearch
RefInfoAgda.Auto.Syntax
reflClosAgda.TypeChecking.SizedTypes.WarshallSolver
ReflectedAgda.Syntax.Common
registerInteractionPointAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
ReifiesToAgda.Syntax.Translation.InternalToAbstract
ReifyAgda.Syntax.Translation.InternalToAbstract
reifyAgda.Syntax.Translation.InternalToAbstract
reifyDisplayFormPAgda.Syntax.Translation.InternalToAbstract
reifyElimToExprAgda.Interaction.BasicOps
reifyPatternsAgda.Syntax.Translation.InternalToAbstract
reifyUnblockedAgda.Syntax.Translation.InternalToAbstract
reifyWhenAgda.Syntax.Translation.InternalToAbstract
reintroduceEllipsisAgda.Syntax.Concrete.Pattern
rejectUnknownFieldsAgda.Interaction.JSON
RelAgda.TypeChecking.Primitive
RelatedAgda.Syntax.Common
relatedAgda.Utils.PartialOrd
relativizeAbsolutePathAgda.Utils.FileName
RelevanceAgda.Syntax.Common
RelevanceAttributeAgda.Syntax.Concrete.Attribute
relevanceAttributesAgda.Syntax.Concrete.Attribute
relevanceAttributeTableAgda.Syntax.Concrete.Attribute
RelevanceMismatchAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RelevantAgda.Syntax.Common
relevantInAgda.TypeChecking.Free
relevantInIgnoringSortAnnAgda.TypeChecking.Free
relOfConstAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
relToDontCareAgda.TypeChecking.Substitute
RelView 
1 (Type/Class)Agda.TypeChecking.Rewriting
2 (Data Constructor)Agda.TypeChecking.Rewriting
relViewAgda.TypeChecking.Rewriting
relViewCoreAgda.TypeChecking.Rewriting
relViewDeltaAgda.TypeChecking.Rewriting
relViewTelAgda.TypeChecking.Rewriting
relViewTypeAgda.TypeChecking.Rewriting
relViewType'Agda.TypeChecking.Rewriting
RemoteMetaStoreAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RemoteMetaVariable 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Remove 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
removeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
RemoveHighlightingAgda.Interaction.Response
removeInteractionPointAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
removeLoneSigAgda.Syntax.Concrete.Definitions.Monad
removeNameFromScopeAgda.Syntax.Scope.Base
removeNodeAgda.Utils.Graph.AdjacencyMap.Unidirectional
removeNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
removeOldInteractionScopeAgda.Interaction.InteractionTop
removeParenPAgda.Syntax.Concrete
removeSucsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
RemoveTokenBasedHighlightingAgda.Interaction.Response
removevarAgda.Auto.CaseSplit
RenAgda.Syntax.Abstract
renAgda.Auto.CaseSplit
renameAgda.Auto.Syntax
renameCanonicalNamesAgda.Syntax.Scope.Base
renameNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
renameNodesMonotonicAgda.Utils.Graph.AdjacencyMap.Unidirectional
renameOffsetAgda.Auto.Syntax
renamePAgda.TypeChecking.Substitute
renameTelAgda.TypeChecking.Telescope
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
renamingAgda.TypeChecking.Substitute
Renaming'Agda.Syntax.Common
RenamingDirectiveAgda.Syntax.Concrete
RenamingDirective'Agda.Syntax.Common
renamingRAgda.TypeChecking.Substitute
rEndAgda.Syntax.Position
rEnd'Agda.Syntax.Position
render 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
renderStyleAgda.Utils.Pretty
renderSuffixAgda.Utils.Suffix
renFixityAgda.Syntax.Common
renFromAgda.Syntax.Common
renModulesAgda.Syntax.Abstract
renNamesAgda.Syntax.Abstract
renToAgda.Syntax.Common
renToRangeAgda.Syntax.Common
reorderAgda.Compiler.JS.Compiler
reorder'Agda.Compiler.JS.Compiler
reorderTelAgda.TypeChecking.Telescope
reorderTel_Agda.TypeChecking.Telescope
repeatAgda.Utils.List1
RepeatedVariablesInPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
repeatWhileAgda.Utils.Function
repeatWhileMAgda.Utils.Function
repl 
1 (Function)Agda.Compiler.Common
2 (Function)Agda.Interaction.AgdaTop
ReplaceAgda.Auto.CaseSplit
replaceAgda.Auto.CaseSplit
replace'Agda.Auto.CaseSplit
replaceEmptyNameAgda.Syntax.Internal
replacementCharAgda.Utils.Char
replaceModuleExtensionAgda.Interaction.FindFile
replacepAgda.Auto.CaseSplit
replaceSurrogateCodePointAgda.Utils.Char
ReplaceWithAgda.Auto.CaseSplit
replInteractorAgda.Main
reportResultAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReportSAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reportSAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reportSDocAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reportSLnAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReqArgAgda.Interaction.Options
requireAllowExecAgda.TypeChecking.Unquote
requireCubicalAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
requireGuardedAgda.TypeChecking.Lock
requireLevelsAgda.TypeChecking.Level
requireOptionRewritingAgda.TypeChecking.Rewriting
ResAgda.TypeChecking.MetaVars
resetAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
resetAllStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
resetLayoutStatusAgda.Syntax.Parser.Monad
resetStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
resolvedBindingSourceAgda.Syntax.Scope.Base
ResolvedNameAgda.Syntax.Scope.Base
resolvedVarAgda.Syntax.Scope.Base
resolveModuleAgda.Syntax.Scope.Monad
resolveNameAgda.Syntax.Scope.Monad
resolveName'Agda.Syntax.Scope.Monad
resolveUnknownInstanceDefsAgda.TypeChecking.Telescope
respInScopeAgda.Interaction.Response
respLetValueAgda.Interaction.Response
ResponseAgda.Interaction.Response
responseAgda.Interaction.EmacsCommand
ResponseContextEntry 
1 (Type/Class)Agda.Interaction.Response
2 (Data Constructor)Agda.Interaction.Response
respOrigNameAgda.Interaction.Response
respReifNameAgda.Interaction.Response
respTypeAgda.Interaction.Response
Resp_ClearHighlightingAgda.Interaction.Response
Resp_ClearRunningInfoAgda.Interaction.Response
Resp_DisplayInfoAgda.Interaction.Response
Resp_DoneAbortingAgda.Interaction.Response
Resp_DoneExitingAgda.Interaction.Response
Resp_GiveActionAgda.Interaction.Response
Resp_HighlightingInfoAgda.Interaction.Response
Resp_InteractionPointsAgda.Interaction.Response
Resp_JumpToErrorAgda.Interaction.Response
Resp_MakeCaseAgda.Interaction.Response
Resp_RunningInfoAgda.Interaction.Response
Resp_SolveAllAgda.Interaction.Response
Resp_StatusAgda.Interaction.Response
Restore 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
restorePostScopeStateAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
restrictLocalPrivateAgda.Syntax.Scope.Base
restrictPrivateAgda.Syntax.Scope.Base
restrictToAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
ResultAgda.Termination.TermCheck
RetractAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
returnExprAgda.Syntax.Concrete
returnTCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reverseAgda.Utils.List1
ReversedSuffixAgda.Utils.List
reversePAgda.Utils.Permutation
revisitRecordPatternTranslationAgda.TypeChecking.Rules.Decl
revLiftAgda.Interaction.InteractionTop
revLiftTCAgda.Interaction.InteractionTop
rewContextAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewFromClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewPatsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewRHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Rewrite 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Interaction.Base
rewriteAgda.TypeChecking.Rewriting
RewriteAmbiguousRulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteAmbiguousRules_Agda.Interaction.Options.Warnings
RewriteEqn 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
RewriteEqn'Agda.Syntax.Common
rewriteExprsAgda.Syntax.Abstract
RewriteMaybeNonConfluentAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteMaybeNonConfluent_Agda.Interaction.Options.Warnings
RewriteMissingRuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteMissingRule_Agda.Interaction.Options.Warnings
RewriteNonConfluentAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteNonConfluent_Agda.Interaction.Options.Warnings
RewritePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
rewriteRelationDomAgda.TypeChecking.Rewriting
RewriteRHSAgda.Syntax.Abstract
rewriteRHSAgda.Syntax.Abstract
RewriteRHSSAgda.Syntax.Abstract
RewriteRule 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteRuleMapAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteRulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewriteStrippedPatsAgda.Syntax.Abstract
rewriteWhereDeclsAgda.Syntax.Abstract
rewriteWithAgda.TypeChecking.Rewriting
rewTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
RhsAgda.Utils.Haskell.Syntax
RHS'Agda.Syntax.Concrete
rhsConcreteAgda.Syntax.Abstract
rhsExprAgda.Syntax.Abstract
RHSSAgda.Syntax.Abstract
RHSSpineAgda.Syntax.Abstract
rhsSpineAgda.Syntax.Abstract
ribbonsPerLineAgda.Utils.Pretty
RICheckElimAgda.Auto.Syntax
RICheckProjIndexAgda.Auto.Syntax
RICopyInfoAgda.Auto.Syntax
rieDefFreeVarsAgda.Auto.Syntax
rieEqReasoningConstsAgda.Auto.Syntax
rieHintsAgda.Auto.Syntax
RIEnvAgda.Auto.Syntax
RIEqRStateAgda.Auto.Syntax
RightAssocAgda.Syntax.Common
RightDisjunctAgda.Auto.NarrowingSearch
rightExprAgda.TypeChecking.SizedTypes.Syntax
rightIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
rightMarginAgda.Syntax.Position
RightOperandCtxAgda.Syntax.Fixity
rightsAgda.Utils.List1
Rigid 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.Utils.Warshall
3 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
4 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
5 (Data Constructor)Agda.TypeChecking.SizedTypes
rigidAgda.TypeChecking.SizedTypes.Syntax
RigidId 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
rigidIdAgda.TypeChecking.SizedTypes.Syntax
rigidIndexAgda.TypeChecking.SizedTypes.Solve
rigidNameAgda.TypeChecking.SizedTypes.Solve
RigidOfAgda.TypeChecking.SizedTypes.Syntax
RigidsAgda.TypeChecking.SizedTypes.Syntax
rigidsAgda.TypeChecking.SizedTypes.Syntax
rigidVarsAgda.TypeChecking.Free
rigidVarsNotContainedInAgda.TypeChecking.MetaVars.Occurs
RIInferredTypeUnknownAgda.Auto.Syntax
RIIotaStepAgda.Auto.Syntax
riMainCxtLengthAgda.Auto.Syntax
RIMainInfoAgda.Auto.Syntax
riMainIotaAgda.Auto.Syntax
riMainTypeAgda.Auto.Syntax
RINotConstructorAgda.Auto.Syntax
RIPickSubsvarAgda.Auto.Syntax
RIUnifInfoAgda.Auto.Syntax
RIUsedVarsAgda.Auto.Syntax
RLiteralAgda.Syntax.Literal
rmAgda.Auto.NarrowingSearch
rmvInstantiationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rmvJudgementAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rmvModalityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rollbackAgda.Syntax.Parser.LookAhead
RollBackMetasAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
rootNameModuleAgda.Interaction.FindFile
roundFixBracketsAgda.Syntax.Fixity
rowAgda.Termination.SparseMatrix
rowdescrAgda.Utils.Warshall
rowsAgda.Termination.SparseMatrix
rparenAgda.Utils.Pretty
rStartAgda.Syntax.Position
rStart'Agda.Syntax.Position
RstFileTypeAgda.Syntax.Common
RStringAgda.Syntax.Common
rtmErrorAgda.Compiler.MAlonzo.Misc
rtmHoleAgda.Compiler.MAlonzo.Misc
rtmQualAgda.Compiler.MAlonzo.Misc
rtmUnreachableErrorAgda.Compiler.MAlonzo.Misc
rtmVarAgda.Compiler.MAlonzo.Misc
rToRAgda.Interaction.Highlighting.Range
rtrimAgda.Utils.String
runAbsToConAgda.Syntax.Translation.AbstractToConcrete
runAgdaAgda.Main
runAgda'Agda.Main
runAgdaWithOptionsAgda.Main
runBlockedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runChangeAgda.Utils.Update
runChangeTAgda.Utils.Update
runFailAgda.Utils.Fail
runFail_Agda.Utils.Fail
runFreeAgda.TypeChecking.Free
runFreeMAgda.TypeChecking.Free.Lazy
runGetStateAgda.TypeChecking.Serialise.Base
runHighlighterAgda.Interaction.Highlighting.FromAbstract
runHsCompileTAgda.Compiler.MAlonzo.Misc
runHsCompileT'Agda.Compiler.MAlonzo.Misc
runIMAgda.Interaction.Monad
runInteractionAgda.Interaction.InteractionTop
runInteractionLoopAgda.Interaction.CommandLine
runLexActionAgda.Syntax.Parser.Alex
runListTAgda.Utils.ListT
runLookAheadAgda.Syntax.Parser.LookAhead
RunMetaOccursCheck 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runMListTAgda.Utils.ListT
runNamesAgda.TypeChecking.Names
runNamesTAgda.TypeChecking.Names
runNiceAgda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
runNLMAgda.TypeChecking.Rewriting.NonLinMatch
runOptMAgda.Interaction.Options
runPAgda.Interaction.Library.Parse
runPMAgda.TypeChecking.Warnings
runPMIOAgda.Syntax.Parser
runPureConversionAgda.TypeChecking.Conversion.Pure
RunRecordPatternTranslation 
1 (Type/Class)Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor)Agda.TypeChecking.CompiledClause.Compile
runReduceFAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runReduceMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runRefCreateEnvAgda.Auto.NarrowingSearch
runSafeTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runStConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTCMPrettyErrorsAgda.Main
runTCMTopAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTCMTop'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTerAgda.Termination.Monad
runTerDefaultAgda.Termination.Monad
runUndoAgda.Auto.NarrowingSearch
runUnifyLogTAgda.TypeChecking.Rules.LHS.Unify.Types
runUnquoteMAgda.TypeChecking.Unquote
runUpdaterAgda.Utils.Update
runUpdaterTAgda.Utils.Update
RVarAgda.Utils.Warshall