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 |
RawName | Agda.Syntax.Common |
rawNameToString | Agda.Syntax.Common |
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 |
readIORef | Agda.Utils.IORef |
readline | Agda.Interaction.Monad |
readM | Agda.Utils.Monad |
readModifyIORef' | Agda.Utils.IORef |
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 |
rebindName | Agda.Syntax.Scope.Monad |
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 (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 |
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 | 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 |
reduceDefCopy | 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 |
reifyUnquoted | Agda.TypeChecking.Unquote |
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 |
RelView | |
1 (Type/Class) | Agda.TypeChecking.Rewriting |
2 (Data Constructor) | Agda.TypeChecking.Rewriting |
relView | Agda.TypeChecking.Rewriting |
relViewCore | Agda.TypeChecking.Rewriting |
relViewDelta | Agda.TypeChecking.Rewriting |
relViewTel | Agda.TypeChecking.Rewriting |
relViewType | Agda.TypeChecking.Rewriting |
relViewType' | Agda.TypeChecking.Rewriting |
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 |
removeNameFromScope | Agda.Syntax.Scope.Base |
removeNode | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
removeOldInteractionScope | Agda.Interaction.InteractionTop |
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.Abstract |
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 |
repeatWhile | Agda.Utils.Function |
repeatWhileM | Agda.Utils.Function |
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 |
resolveUnknownInstanceDefs | Agda.TypeChecking.Telescope |
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 |
rewContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
rewLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
rewName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
rewRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Rewrite | Agda.Interaction.BasicOps |
rewrite | Agda.TypeChecking.Rewriting |
RewriteEqn | Agda.Syntax.Concrete |
RewritePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
RewriteRHS | Agda.Syntax.Abstract |
RewriteRule | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
RewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
rewriteWith | Agda.TypeChecking.Rewriting |
rewType | Agda.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 |
RhsUsesDottedVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
rigidlyConstrainedMetas | Agda.TypeChecking.InstanceArguments |
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 |
runExceptT | Agda.Utils.Except |
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 |
runReduceF | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
runTer | Agda.Termination.Monad |
runTerDefault | Agda.Termination.Monad |
runTests | Agda.Utils.TestHelpers |
runUndo | Agda.Auto.NarrowingSearch |
runUnquoteM | Agda.TypeChecking.Unquote |
runUpdater | Agda.Utils.Update |
RVar | Agda.Utils.Warshall |