Agda-2.6.1.3: 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
raiseFromAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Range 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
3 (Type/Class)Agda.Interaction.Highlighting.Range
4 (Data Constructor)Agda.Interaction.Highlighting.Range
Range'Agda.Syntax.Position
RangeAndPragma 
1 (Type/Class)Agda.Syntax.Translation.AbstractToConcrete
2 (Data Constructor)Agda.Syntax.Translation.AbstractToConcrete
Ranged 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
rangedThingAgda.Syntax.Common
rangeFileAgda.Syntax.Position
rangeIntervalsAgda.Syntax.Position
rangeInvariant 
1 (Function)Agda.Syntax.Position
2 (Function)Agda.Interaction.Highlighting.Range
rangeOfAgda.Syntax.Common
Ranges 
1 (Type/Class)Agda.Interaction.Highlighting.Range
2 (Data Constructor)Agda.Interaction.Highlighting.Range
rangesAgda.Interaction.Highlighting.Precise
rangesInvariantAgda.Interaction.Highlighting.Range
rangesToPositionsAgda.Interaction.Highlighting.Range
rangeToEndPointsAgda.Interaction.Highlighting.Range
rangeToIntervalAgda.Syntax.Position
rangeToIntervalWithFileAgda.Syntax.Position
rangeToPositionsAgda.Interaction.Highlighting.Range
rationalAgda.Utils.Pretty
RawAppAgda.Syntax.Concrete
RawAppPAgda.Syntax.Concrete
RawNameAgda.Syntax.Common
rawNameToStringAgda.Syntax.Common
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
ReadFileErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
readFilePMAgda.Syntax.Parser
readFromCachedLogAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
readInterfaceAgda.Interaction.Imports
readInterface'Agda.Interaction.Imports
readIORefAgda.Utils.IORef
readlineAgda.Interaction.Monad
readMAgda.Utils.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.Rewriting.NonLinMatch
ReallyNotBlockedAgda.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
RecDefAgda.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
recheckAbstractClauseAgda.Interaction.MakeCase
recInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecNameAgda.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
reconstructParametersAgda.TypeChecking.ReconstructParameters
reconstructParametersInEqViewAgda.TypeChecking.ReconstructParameters
reconstructParametersInTelAgda.TypeChecking.ReconstructParameters
reconstructParametersInTypeAgda.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
RecordDef 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Reflected
recordFieldNamesAgda.TypeChecking.Records
RecordFlexAgda.TypeChecking.Rules.LHS.Problem
recordModuleAgda.TypeChecking.Records
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
recRecursiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecSigAgda.Syntax.Abstract
recTelAgda.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
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
redReturnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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
reduceIApplyAgda.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
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
refineMetaAgda.Interaction.CommandLine
RefInfoAgda.Auto.Syntax
reflClosAgda.TypeChecking.SizedTypes.WarshallSolver
ReflectedAgda.Syntax.Common
registerInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
RelAgda.TypeChecking.Primitive
RelatedAgda.Syntax.Common
relatedAgda.Utils.PartialOrd
RelevanceAgda.Syntax.Common
relevanceActionAgda.TypeChecking.CheckInternal
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
relevantInIgnoringNonvariantAgda.TypeChecking.Polarity
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
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
removeNameFromScopeAgda.Syntax.Scope.Base
removeNodeAgda.Utils.Graph.AdjacencyMap.Unidirectional
removeNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
removeOldInteractionScopeAgda.Interaction.InteractionTop
removePrivatesAgda.Interaction.Imports
removeSingletonRawAppPAgda.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
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
renamingRAgda.TypeChecking.Substitute
rEndAgda.Syntax.Position
rEnd'Agda.Syntax.Position
renderAgda.Utils.Pretty
renderStyleAgda.Utils.Pretty
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
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
replaceModuleExtensionAgda.Interaction.FindFile
replacepAgda.Auto.CaseSplit
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
requireCubicalAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
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
restartOptionsAgda.Interaction.Options
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
ResultAgda.Termination.TermCheck
retryConstraintsAgda.Interaction.CommandLine
ReturnAgda.Interaction.CommandLine
returnTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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
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
RewriteRHSAgda.Syntax.Abstract
rewriteRHSAgda.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
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.Pretty
rightMarginAgda.Syntax.Position
RightOperandCtxAgda.Syntax.Fixity
Rigid 
1 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class)Agda.Utils.Warshall
4 (Data Constructor)Agda.Utils.Warshall
5 (Data Constructor)Agda.TypeChecking.SizedTypes
rigidAgda.TypeChecking.SizedTypes.Syntax
RigidId 
1 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.Utils.Warshall
rigidIdAgda.TypeChecking.SizedTypes.Syntax
rigidIndexAgda.TypeChecking.SizedTypes.Solve
rigidNameAgda.TypeChecking.SizedTypes.Solve
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
rmAgda.Auto.NarrowingSearch
rollbackAgda.Syntax.Parser.LookAhead
RollBackMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rootNameModuleAgda.Interaction.FindFile
rootPathAgda.Utils.FileName
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
rtmIncompleteMatchAgda.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
runChangeAgda.Utils.Update
runChangeTAgda.Utils.Update
runExceptTAgda.Utils.Except
runFailAgda.Utils.Fail
runFail_Agda.Utils.Fail
runFreeAgda.TypeChecking.Free
runFreeMAgda.TypeChecking.Free.Lazy
runGetStateAgda.TypeChecking.Serialise.Base
runIMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad, Agda.Compiler.Backend
runInteractionAgda.Interaction.InteractionTop
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
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
runUnquoteMAgda.TypeChecking.Unquote
runUpdaterAgda.Utils.Update
runUpdaterTAgda.Utils.Update
RVarAgda.Utils.Warshall