Agda-2.6.2.2.20221128: 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.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
readTextFileAgda.Utils.IO.UTF8
reallyAllReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReallyDontExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reallyDontExpandLastAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
recalcAgda.Auto.NarrowingSearch
recalcsAgda.Auto.NarrowingSearch
reccalcAgda.Auto.NarrowingSearch
RecCheckAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
recClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recCompAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recConHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recConstructorAgda.Syntax.Common
RecDefAgda.Syntax.Abstract
RecDefSAgda.Syntax.Abstract
recEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recEtaEquality'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recHasEtaAgda.Syntax.Common
recheckAbstractClauseAgda.Interaction.MakeCase
recheckBecausePragmaOptionsChangedAgda.Interaction.Options
recInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recInductiveAgda.Syntax.Common
recMutualAgda.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
recNamedConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
RecordAssignAgda.Syntax.Abstract
RecordAssignmentAgda.Syntax.Concrete
RecordAssignmentsAgda.Syntax.Concrete
RecordAssignsAgda.Syntax.Abstract
RecordConAgda.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
RecordDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recordFieldWarningToErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
recPatternAgda.Syntax.Common
recPatternMatchingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recRecursiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecSigAgda.Syntax.Abstract
RecSigSAgda.Syntax.Abstract
recTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
redBindAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redoChecksAgda.Interaction.BasicOps
redPredAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redReturnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redReturnNoSimplAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
redStAgda.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
reduceAgda.TypeChecking.Reduce
reduce'Agda.TypeChecking.Reduce
reduce2LamAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
reduceAllDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReduceAndEtaContractAgda.TypeChecking.MetaVars
reduceAndEtaContractAgda.TypeChecking.MetaVars
reduceBAgda.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
reducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceDefCopyAgda.TypeChecking.Reduce
reduceDefCopyTCMAgda.TypeChecking.Reduce
ReduceDefsAgda.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
reduceEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceHeadAgda.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
reduceProjectionLikeAgda.TypeChecking.ProjectionLike
reduceQuotedTermAgda.TypeChecking.Unquote
reduceStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
RelevantAgda.Syntax.Common
relevantInAgda.TypeChecking.Free
relevantInIgnoringSortAnnAgda.TypeChecking.Free
relOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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
removeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
RemoveHighlightingAgda.Interaction.Response
removeInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Concrete
3 (Type/Class)Agda.Auto.Syntax
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
ReportSAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reportSAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reportSDocAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reportSLnAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReqArgAgda.Interaction.Options
requireAllowExecAgda.TypeChecking.Unquote
requireCubicalAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
requireGuardedAgda.TypeChecking.Lock
requireLevelsAgda.TypeChecking.Level
requireOptionRewritingAgda.TypeChecking.Rewriting
ResAgda.TypeChecking.MetaVars
resetAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
resetAllStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
resetLayoutStatusAgda.Syntax.Parser.Monad
resetStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
reverseAgda.Utils.List1
ReversedSuffixAgda.Utils.List
reversePAgda.Utils.Permutation
revisitRecordPatternTranslationAgda.TypeChecking.Rules.Decl
revLiftAgda.Interaction.InteractionTop
revLiftTCAgda.Interaction.InteractionTop
rewContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewFromClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewPatsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Rewrite 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Interaction.Base
rewriteAgda.TypeChecking.Rewriting
RewriteAmbiguousRulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
RewriteMaybeNonConfluent_Agda.Interaction.Options.Warnings
RewriteMissingRuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteMissingRule_Agda.Interaction.Options.Warnings
RewriteNonConfluentAgda.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
rewriteRelationDomAgda.TypeChecking.Rewriting
RewriteRHSAgda.Syntax.Abstract
rewriteRHSAgda.Syntax.Abstract
RewriteRHSSAgda.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
RewriteRuleMapAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteRulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewriteStrippedPatsAgda.Syntax.Abstract
rewriteWhereDeclsAgda.Syntax.Abstract
rewriteWithAgda.TypeChecking.Rewriting
rewTypeAgda.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
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.TypeChecking.Monad, Agda.Compiler.Backend
rmvJudgementAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rmvModalityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rollbackAgda.Syntax.Parser.LookAhead
RollBackMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
runReduceMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runRefCreateEnvAgda.Auto.NarrowingSearch
runSafeTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runStConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTCMPrettyErrorsAgda.Main
runTCMTopAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTCMTop'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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