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

Index - R

R 
1 (Data Constructor)Agda.Utils.Map
2 (Type/Class)Agda.TypeChecking.Serialise.Base
raiseAgda.TypeChecking.Substitute
raiseDBPAgda.Termination.Monad
raiseFromAgda.TypeChecking.Substitute
RaiseNLPAgda.TypeChecking.Rewriting.NonLinMatch
raiseNLPAgda.TypeChecking.Rewriting.NonLinMatch
raiseNLPFromAgda.TypeChecking.Rewriting.NonLinMatch
raisePatVarsAgda.TypeChecking.Pretty
raiseSAgda.TypeChecking.Substitute
Range 
1 (Type/Class)Agda.Syntax.Position
2 (Type/Class)Agda.Interaction.Highlighting.Range
3 (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
rangeToPositionsAgda.Interaction.Highlighting.Range
rationalAgda.Utils.Pretty
RawAppAgda.Syntax.Concrete
RawAppPAgda.Syntax.Concrete
RawNameAgda.Syntax.Common
rawNameToStringAgda.Syntax.Common
rbraceAgda.Utils.Pretty
rbrackAgda.Utils.Pretty
RConstAgda.Utils.Warshall
reAbsAgda.TypeChecking.Substitute
reachableAgda.Utils.Graph.AdjacencyMap.Unidirectional
reachableFromAgda.Utils.Graph.AdjacencyMap.Unidirectional
readBinaryFile'Agda.Utils.IO.Binary
readFromCachedLogAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad
readInterfaceAgda.Interaction.Imports
readIORefAgda.Utils.IORef
readlineAgda.Interaction.Monad
readMAgda.Utils.Monad
readModifyIORef'Agda.Utils.IORef
ReadPAgda.Utils.Parser.ReadP
readParseAgda.Interaction.InteractionTop
readsToParseAgda.Interaction.InteractionTop
ReadTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
readTextFileAgda.Utils.IO.UTF8
ReallyNotBlockedAgda.Syntax.Internal
reallyUnLevelViewAgda.TypeChecking.Level
reasonAgda.Utils.QuickCheck
rebindNameAgda.Syntax.Scope.Monad
Rec 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recalcAgda.Auto.NarrowingSearch
recalcsAgda.Auto.NarrowingSearch
reccalcAgda.Auto.NarrowingSearch
RecCheckAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
recClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecDef 
1 (Data Constructor)Agda.Syntax.Concrete.Definitions
2 (Data Constructor)Agda.Syntax.Abstract
recEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recEtaEquality'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recNamedConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
RecordAssignAgda.Syntax.Abstract
RecordAssignmentAgda.Syntax.Concrete
RecordAssignmentsAgda.Syntax.Concrete
RecordAssignsAgda.Syntax.Abstract
RecordConAgda.TypeChecking.Datatypes
RecordDefAgda.Syntax.Reflected
recordFieldNamesAgda.TypeChecking.Records
RecordFlexAgda.TypeChecking.Rules.LHS.Problem
recordModuleAgda.TypeChecking.Records
RecordModuleIFS 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recordPatternToProjectionsAgda.TypeChecking.RecordPatterns
RecordsAgda.TypeChecking.MetaVars
RecordSigAgda.Syntax.Concrete
RecP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recRecursiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recRecursive_Agda.TypeChecking.Records
RecSigAgda.Syntax.Abstract
recTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecUpdate 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recurseExprAgda.Syntax.Abstract.Views
recursiveAgda.Termination.RecCheck
recursivelyShrinkAgda.Utils.QuickCheck
recursiveRecordAgda.TypeChecking.Records
redBindAgda.TypeChecking.Primitive
redEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
redReturnAgda.TypeChecking.Primitive
redStAgda.TypeChecking.Monad.Base, 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
reduceBAgda.TypeChecking.Reduce
reduceB'Agda.TypeChecking.Reduce
Reduced 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceDefCopyAgda.TypeChecking.Reduce
ReduceEnv 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceHeadAgda.TypeChecking.Reduce
reduceHead'Agda.TypeChecking.Reduce
ReduceM 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceProjectionLikeAgda.TypeChecking.ProjectionLike
reduceQuotedTermAgda.TypeChecking.Unquote
RefCreateEnvAgda.Auto.NarrowingSearch
RefinableAgda.Auto.NarrowingSearch
RefineAgda.Interaction.InteractionTop
refine 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Interaction.BasicOps
refinementsAgda.Auto.NarrowingSearch
refineMetaAgda.Interaction.CommandLine
RefInfoAgda.Auto.Syntax
reflClosAgda.TypeChecking.SizedTypes.WarshallSolver
refreshStrAgda.Interaction.InteractionTop
registerInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
ReifyAgda.Syntax.Translation.InternalToAbstract
reifyAgda.Syntax.Translation.InternalToAbstract
reifyPatternsAgda.Syntax.Translation.InternalToAbstract
reifyWhenAgda.Syntax.Translation.InternalToAbstract
Rel 
1 (Data Constructor)Agda.Compiler.Epic.Interface
2 (Type/Class)Agda.TypeChecking.Primitive
RelatedAgda.Syntax.Fixity
relatedAgda.Utils.PartialOrd
RelationAgda.TypeChecking.SizedTypes.Tests
RelativeToAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Relevance 
1 (Type/Class)Agda.Syntax.Common
2 (Type/Class)Agda.Compiler.Epic.Interface
RelevanceMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
relevanciesAgda.Compiler.Epic.Erasure
RelevantAgda.Syntax.Common
relevantAgda.Compiler.Epic.Erasure
RelevantArgsAgda.Compiler.Epic.Interface
relevantArgsAgda.Compiler.Epic.Interface
relevantIn 
1 (Function)Agda.TypeChecking.Free.Old
2 (Function)Agda.TypeChecking.Free
relevantInIgnoringNonvariantAgda.TypeChecking.Polarity
relevantInIgnoringSortAnn 
1 (Function)Agda.TypeChecking.Free.Old
2 (Function)Agda.TypeChecking.Free
relevantVars 
1 (Function)Agda.TypeChecking.Free.Old
2 (Function)Agda.TypeChecking.Free
relOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
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
remForcedAgda.Compiler.Epic.Forcing
removeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
removeInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
removeNameFromScopeAgda.Syntax.Scope.Base
removeNodeAgda.Utils.Graph.AdjacencyMap.Unidirectional
removeOldInteractionScopeAgda.Interaction.InteractionTop
removeOnlyQualifiedAgda.Syntax.Scope.Base
removePrivatesAgda.Interaction.Imports
removeSucsAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
removeUnusedAgda.Compiler.Epic.Erasure
removevarAgda.Auto.CaseSplit
RenAgda.Syntax.Abstract
renAgda.Auto.CaseSplit
renameAgda.Auto.CaseSplit
renameCanonicalNamesAgda.Syntax.Scope.Base
renamePAgda.TypeChecking.Telescope
renamepAgda.Auto.CaseSplit
Renaming 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
renamingAgda.TypeChecking.Telescope
Renaming'Agda.Syntax.Common
renamingRAgda.TypeChecking.Telescope
rEndAgda.Syntax.Position
rEnd'Agda.Syntax.Position
renderAgda.Utils.Pretty
renderStyleAgda.Utils.Pretty
renFromAgda.Syntax.Common
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
repeatWhileAgda.Utils.Function
repeatWhileMAgda.Utils.Function
replAgda.Compiler.Common
replaceAgda.Auto.CaseSplit
replaceAtAgda.Compiler.Epic.CompileState
replaceEmptyNameAgda.Syntax.Internal
replaceForcedAgda.Compiler.Epic.Forcing
replaceFunCCAgda.Compiler.Epic.Injection
replacepAgda.Auto.CaseSplit
replayAgda.Utils.QuickCheck
reportAgda.Compiler.Epic.Forcing
reportSAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
reportSDoc 
1 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
2 (Function)Agda.TypeChecking.Reduce.Monad
reportSLn 
1 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
2 (Function)Agda.TypeChecking.Reduce.Monad
requireLevelsAgda.TypeChecking.Level
requireOptionRewritingAgda.TypeChecking.Rewriting
ResAgda.TypeChecking.MetaVars
resetAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
resetAllStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resetNameSupplyAgda.Compiler.Epic.CompileState
resetStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resizeAgda.Utils.QuickCheck
resizeConfAgda.TypeChecking.Test.Generators
ResolvedNameAgda.Syntax.Scope.Monad
resolveModuleAgda.Syntax.Scope.Monad
resolveNameAgda.Syntax.Scope.Monad
resolveName'Agda.Syntax.Scope.Monad
resolveUnknownInstanceDefsAgda.TypeChecking.Telescope
ResponseAgda.Interaction.Response
responseAgda.Interaction.EmacsCommand
Resp_ClearHighlightingAgda.Interaction.Response
Resp_ClearRunningInfoAgda.Interaction.Response
Resp_DisplayInfoAgda.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
restPatsAgda.TypeChecking.Rules.LHS.Problem
restrictLocalPrivateAgda.Syntax.Scope.Base
restrictPrivateAgda.Syntax.Scope.Base
restTypeAgda.TypeChecking.Rules.LHS.Problem
Result 
1 (Type/Class)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Termination.TermCheck
retryConstraintsAgda.Interaction.CommandLine
ReturnAgda.Interaction.CommandLine
returnBlockAgda.Compiler.JS.Parser
returnTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reverseCCBodyAgda.Compiler.Epic.FromAgda
reversePAgda.Utils.Permutation
revLiftAgda.Interaction.InteractionTop
rewArityAgda.TypeChecking.Rewriting
rewContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
rewLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
rewNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
rewRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RewriteAgda.Interaction.BasicOps
rewriteAgda.TypeChecking.Rewriting
rewriteAfterAgda.TypeChecking.Reduce
RewriteEqnAgda.Syntax.Concrete
RewritePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
RewriteRHSAgda.Syntax.Abstract
RewriteRule 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RewriteRuleMapAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RewriteRulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
rewriteWithAgda.TypeChecking.Rewriting
rewTypeAgda.TypeChecking.Monad.Base, 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
RHS'Agda.Syntax.Concrete
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.Fixity
RightDisjunctAgda.Auto.NarrowingSearch
rightDistributiveAgda.Utils.TestHelpers
rightExprAgda.TypeChecking.SizedTypes.Syntax
RightHandSideAgda.Syntax.Translation.ConcreteToAbstract
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.MetaVars.Occurs
6 (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
rigidlyConstrainedMetasAgda.TypeChecking.InstanceArguments
rigidNameAgda.TypeChecking.SizedTypes.Solve
RigidsAgda.TypeChecking.SizedTypes.Syntax
rigidsAgda.TypeChecking.SizedTypes.Syntax
rigidVars 
1 (Function)Agda.TypeChecking.Free.Old
2 (Function)Agda.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.CaseSplit
rollbackAgda.Syntax.Parser.LookAhead
rootNameAgda.Utils.FileName
roundFixBracketsAgda.Syntax.Fixity
rowAgda.Termination.SparseMatrix
rowdescrAgda.Utils.Warshall
rowsAgda.Termination.SparseMatrix
rparenAgda.Utils.Pretty
rStartAgda.Syntax.Position
rStart'Agda.Syntax.Position
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
runAgdaWithOptionsAgda.Main
runChangeAgda.Utils.Update
runCompileTAgda.Compiler.UHC.CompileState
runExceptionTAgda.TypeChecking.Monad.Exception
runExceptTAgda.Utils.Except
runFreeAgda.TypeChecking.Free
runGetStateAgda.TypeChecking.Serialise.Base
runIMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad
runInteractionAgda.Interaction.InteractionTop
runListTAgda.Utils.ListT
runLookAheadAgda.Syntax.Parser.LookAhead
RunMetaOccursCheck 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runMListTAgda.Utils.ListT
runNiceAgda.Syntax.Concrete.Definitions
runNLMAgda.TypeChecking.Rewriting.NonLinMatch
runOptMAgda.Interaction.Options
runReduceFAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runReduceMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runSafeTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCMPrettyErrorsAgda.Main
runTCMTopAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCMTop'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTerAgda.Termination.Monad
runTerDefaultAgda.Termination.Monad
runTestsAgda.Utils.TestHelpers
runTTAgda.Compiler.UHC.FromAgda
runUndoAgda.Auto.NarrowingSearch
runUnquoteMAgda.TypeChecking.Unquote
runUpdaterAgda.Utils.Update
RVarAgda.Utils.Warshall