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

Index - R

R	Agda.Utils.Map
raise	Agda.TypeChecking.Substitute
raiseDBP	Agda.Termination.Monad
raiseFrom	Agda.TypeChecking.Substitute
raiseS	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
rangedThing	Agda.Syntax.Common
rangeInvariant
1 (Function)	Agda.Syntax.Position
2 (Function)	Agda.Interaction.Highlighting.Range
rangeOf	Agda.Syntax.Common
Ranges
1 (Type/Class)	Agda.Interaction.Highlighting.Range
2 (Data Constructor)	Agda.Interaction.Highlighting.Range
ranges	Agda.Interaction.Highlighting.Precise
rangesInvariant	Agda.Interaction.Highlighting.Range
rangesToPositions	Agda.Interaction.Highlighting.Range
rangeToInterval	Agda.Syntax.Position
rangeToPositions	Agda.Interaction.Highlighting.Range
rational	Agda.Utils.Pretty
RawApp	Agda.Syntax.Concrete
RawAppP	Agda.Syntax.Concrete
rbrace	Agda.Utils.Pretty
rbrack	Agda.Utils.Pretty
RConst	Agda.Utils.Warshall
reAbs	Agda.TypeChecking.Substitute
readBinaryFile'	Agda.Utils.IO.Binary
readInterface	Agda.Interaction.Imports
readline	Agda.Interaction.Monad
readM	Agda.Utils.Monad
ReadP	Agda.Utils.ReadP
readParse	Agda.Interaction.InteractionTop
readsToParse	Agda.Interaction.InteractionTop
readTextFile	Agda.Utils.IO.UTF8
reallyUnLevelView	Agda.TypeChecking.Level
reason	Agda.Utils.QuickCheck
rebuild	Agda.Syntax.Concrete.Operators.Parser
rebuildBinding	Agda.Syntax.Concrete.Operators.Parser
Rec
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
recAbstr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recalc	Agda.Auto.NarrowingSearch
recalcs	Agda.Auto.NarrowingSearch
reccalc	Agda.Auto.NarrowingSearch
RecCheck	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
recClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recCon	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecDef
1 (Data Constructor)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Syntax.Concrete.Definitions
recEtaEquality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recInduction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recMutual	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recNamedCon	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Record
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recordFieldNames	Agda.TypeChecking.Records
RecordFlex	Agda.TypeChecking.Rules.LHS.Problem
recordModule	Agda.TypeChecking.Records
RecordModuleIFS
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
recordPatternToProjections	Agda.TypeChecking.RecordPatterns
Records	Agda.TypeChecking.MetaVars
RecordSig	Agda.Syntax.Concrete
recPars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recRecursive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recRecursive_	Agda.TypeChecking.Records
RecSig	Agda.Syntax.Abstract
recTel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecUpdate
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
recursive
1 (Function)	Agda.Syntax.Concrete.Operators.Parser
2 (Function)	Agda.Termination.RecCheck
recursivelyShrink	Agda.Utils.QuickCheck
recursiveRecord	Agda.TypeChecking.Records
redBind	Agda.TypeChecking.Primitive
redEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
redReturn	Agda.TypeChecking.Primitive
redSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Reduce
1 (Data Constructor)	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class)	Agda.TypeChecking.Reduce
reduce	Agda.TypeChecking.Reduce
reduce'	Agda.TypeChecking.Reduce
reduceB	Agda.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
reduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceDef	Agda.TypeChecking.Reduce
reduceDefCopy	Agda.TypeChecking.Reduce
reduceDef_	Agda.TypeChecking.Reduce
ReduceEnv
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceHead	Agda.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
reduceProjectionLike	Agda.TypeChecking.ProjectionLike
RefCreateEnv	Agda.Auto.NarrowingSearch
Refinable	Agda.Auto.NarrowingSearch
Refine	Agda.Interaction.InteractionTop
refine
1 (Function)	Agda.Compiler.JS.Case
2 (Function)	Agda.Interaction.BasicOps
refinements	Agda.Auto.NarrowingSearch
refineMeta	Agda.Interaction.CommandLine.CommandLine
RefInfo	Agda.Auto.Syntax
reflClos	Agda.TypeChecking.SizedTypes.WarshallSolver
refreshStr	Agda.Interaction.InteractionTop
registerInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
Reify	Agda.Syntax.Translation.InternalToAbstract
reify	Agda.Syntax.Translation.InternalToAbstract
reifyPatterns	Agda.Syntax.Translation.InternalToAbstract
reifyWhen	Agda.Syntax.Translation.InternalToAbstract
reimburse	Agda.TypeChecking.Monad.Benchmark
reimburseTop	Agda.TypeChecking.Monad.Benchmark
Rel
1 (Data Constructor)	Agda.Compiler.Epic.Interface
2 (Type/Class)	Agda.TypeChecking.Primitive
related	Agda.Utils.PartialOrd
Relation	Agda.TypeChecking.SizedTypes.Tests
RelativeTo	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Relevance
1 (Type/Class)	Agda.Syntax.Common
2 (Type/Class)	Agda.Compiler.Epic.Interface
RelevanceMismatch	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
relevancies	Agda.Compiler.Epic.Erasure
Relevant	Agda.Syntax.Common
relevant	Agda.Compiler.Epic.Erasure
RelevantArgs	Agda.Compiler.Epic.Interface
relevantArgs	Agda.Compiler.Epic.Interface
relevantIn	Agda.TypeChecking.Free
relevantInIgnoringNonvariant	Agda.TypeChecking.Polarity
relevantInIgnoringSortAnn	Agda.TypeChecking.Free
relevantVars	Agda.TypeChecking.Free
relOfConst	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
remForced	Agda.Compiler.Epic.Forcing
removeEdge
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
removeInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
removeNode
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
removeOldInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
removeOnlyQualified	Agda.Syntax.Scope.Base
removeSucs	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
removeUnused	Agda.Compiler.Epic.Erasure
removevar	Agda.Auto.CaseSplit
Ren	Agda.Syntax.Scope.Monad
ren	Agda.Auto.CaseSplit
rename	Agda.Auto.CaseSplit
renameCanonicalNames	Agda.Syntax.Scope.Base
renameP	Agda.TypeChecking.Telescope
renamep	Agda.Auto.CaseSplit
Renaming
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
renaming
1 (Function)	Agda.Syntax.Concrete
2 (Function)	Agda.TypeChecking.Telescope
renamingR	Agda.TypeChecking.Telescope
rEnd	Agda.Syntax.Position
render	Agda.Utils.Pretty
renderStyle	Agda.Utils.Pretty
renFrom	Agda.Syntax.Concrete
renTo	Agda.Syntax.Concrete
renToRange	Agda.Syntax.Concrete
reorder	Agda.Compiler.JS.Compiler
reorder'	Agda.Compiler.JS.Compiler
reorderTel	Agda.TypeChecking.Telescope
reorderTel_	Agda.TypeChecking.Telescope
RepeatedVariablesInPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
repl	Agda.Compiler.MAlonzo.Primitives
replace	Agda.Auto.CaseSplit
replaceAt	Agda.Compiler.Epic.CompileState
replaceEmptyName	Agda.Syntax.Internal
replaceForced	Agda.Compiler.Epic.Forcing
replaceFunCC	Agda.Compiler.Epic.Injection
replacep	Agda.Auto.CaseSplit
replay	Agda.Utils.QuickCheck
replicateM	Agda.Utils.Monad
replicateM_	Agda.Utils.Monad
report	Agda.Compiler.Epic.Forcing
reportBenchmarkingDoc	Agda.TypeChecking.Monad.Benchmark
reportBenchmarkingLn	Agda.TypeChecking.Monad.Benchmark
reportPostponing	Agda.TypeChecking.Rules.LHS.Unify
reportS	Agda.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
requireLevels	Agda.TypeChecking.Level
Res	Agda.TypeChecking.MetaVars
resetAllState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resetNameSupply	Agda.Compiler.Epic.CompileState
resetState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resize	Agda.Utils.QuickCheck
resizeConf	Agda.TypeChecking.Test.Generators
ResolvedName	Agda.Syntax.Scope.Monad
resolveModule	Agda.Syntax.Scope.Monad
resolveName	Agda.Syntax.Scope.Monad
resolveName'	Agda.Syntax.Scope.Monad
Response	Agda.Interaction.Response
response	Agda.Interaction.EmacsCommand
Resp_ClearHighlighting	Agda.Interaction.Response
Resp_ClearRunningInfo	Agda.Interaction.Response
Resp_DisplayInfo	Agda.Interaction.Response
Resp_GiveAction	Agda.Interaction.Response
Resp_HighlightingInfo	Agda.Interaction.Response
Resp_InteractionPoints	Agda.Interaction.Response
Resp_JumpToError	Agda.Interaction.Response
Resp_MakeCase	Agda.Interaction.Response
Resp_RunningInfo	Agda.Interaction.Response
Resp_SolveAll	Agda.Interaction.Response
Resp_Status	Agda.Interaction.Response
Restore
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
restPats	Agda.TypeChecking.Rules.LHS.Problem
restrictPrivate	Agda.Syntax.Scope.Base
restType	Agda.TypeChecking.Rules.LHS.Problem
Result
1 (Type/Class)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Termination.TermCheck
retryConstraints	Agda.Interaction.CommandLine.CommandLine
Return	Agda.Interaction.CommandLine.CommandLine
return	Agda.Utils.Monad
returnBlock	Agda.Compiler.JS.Parser
returnTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reverseCCBody	Agda.Compiler.Epic.FromAgda
reverseP	Agda.Utils.Permutation
revLift	Agda.Interaction.InteractionTop
Rewrite	Agda.Interaction.BasicOps
rewrite	Agda.Interaction.BasicOps
RewriteEqn	Agda.Syntax.Concrete
RewriteRHS	Agda.Syntax.Abstract
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
ribbonsPerLine	Agda.Utils.Pretty
RICheckElim	Agda.Auto.Syntax
RICheckProjIndex	Agda.Auto.Syntax
RICopyInfo	Agda.Auto.Syntax
rieDefFreeVars	Agda.Auto.Syntax
rieEqReasoningConsts	Agda.Auto.Syntax
rieHints	Agda.Auto.Syntax
RIEnv	Agda.Auto.Syntax
RIEqRState	Agda.Auto.Syntax
RightAssoc	Agda.Syntax.Fixity
RightDisjunct	Agda.Auto.NarrowingSearch
rightDistributive	Agda.Utils.TestHelpers
rightExpr	Agda.TypeChecking.SizedTypes.Syntax
RightHandSide	Agda.Syntax.Translation.ConcreteToAbstract
rightHH	Agda.TypeChecking.Rules.LHS.Unify
rightMargin	Agda.Syntax.Position
RightOperandCtx	Agda.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
6 (Data Constructor)	Agda.TypeChecking.MetaVars.Occurs
rigid	Agda.TypeChecking.SizedTypes.Syntax
RigidId
1 (Data Constructor)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.Utils.Warshall
rigidId	Agda.TypeChecking.SizedTypes.Syntax
rigidIndex	Agda.TypeChecking.SizedTypes.Solve
rigidName	Agda.TypeChecking.SizedTypes.Solve
Rigids	Agda.TypeChecking.SizedTypes.Syntax
rigids	Agda.TypeChecking.SizedTypes.Syntax
rigidVars	Agda.TypeChecking.Free
rigidVarsNotContainedIn	Agda.TypeChecking.MetaVars.Occurs
RIInferredTypeUnknown	Agda.Auto.Syntax
RIIotaStep	Agda.Auto.Syntax
riMainCxtLength	Agda.Auto.Syntax
RIMainInfo	Agda.Auto.Syntax
riMainIota	Agda.Auto.Syntax
riMainType	Agda.Auto.Syntax
RINotConstructor	Agda.Auto.Syntax
RIPickSubsvar	Agda.Auto.Syntax
RIUnifInfo	Agda.Auto.Syntax
RIUsedVars	Agda.Auto.Syntax
rm	Agda.Auto.CaseSplit
rollback	Agda.Syntax.Parser.LookAhead
rootName	Agda.Utils.FileName
roundFixBrackets	Agda.Syntax.Fixity
row	Agda.Termination.SparseMatrix
rowdescr	Agda.Utils.Warshall
rows	Agda.Termination.SparseMatrix
rparen	Agda.Utils.Pretty
rStart	Agda.Syntax.Position
RString	Agda.Syntax.Common
rteModule	Agda.Compiler.MAlonzo.Compiler
rtmError	Agda.Compiler.MAlonzo.Misc
rtmIncompleteMatch	Agda.Compiler.MAlonzo.Misc
rtmMod	Agda.Compiler.MAlonzo.Misc
rtmQual	Agda.Compiler.MAlonzo.Misc
rtmVar	Agda.Compiler.MAlonzo.Misc
rToR	Agda.Interaction.Highlighting.Range
runAbsToCon	Agda.Syntax.Translation.AbstractToConcrete
runAgda	Agda.Main
runChange	Agda.Utils.Update
runExceptionT	Agda.TypeChecking.Monad.Exception
runIM	Agda.Interaction.Monad
runInteraction	Agda.Interaction.InteractionTop
runLookAhead	Agda.Syntax.Parser.LookAhead
RunMetaOccursCheck
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runNice	Agda.Syntax.Concrete.Definitions
runReduceM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runSafeTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCMTop	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCMTop'	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTerm	Agda.Termination.Monad
runTests	Agda.Utils.TestHelpers
runUndo	Agda.Auto.NarrowingSearch
runUpdater	Agda.Utils.Update
RVar	Agda.Utils.Warshall