| R | Agda.Utils.Map |
| Raise | Agda.TypeChecking.Substitute |
| raise | Agda.TypeChecking.Substitute |
| raiseFrom | Agda.TypeChecking.Substitute |
| Range | |
| 1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 3 (Type/Class) | Agda.Interaction.Highlighting.Range |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Range |
| RangeAndPragma | |
| 1 (Type/Class) | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| rangeInvariant | |
| 1 (Function) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Function) | Agda.Interaction.Highlighting.Range |
| ranges | Agda.Utils.QuickCheck |
| rangeToInterval | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| rational | Agda.Utils.Pretty |
| RawApp | Agda.Syntax.Concrete |
| RawAppP | Agda.Syntax.Concrete |
| RB | Agda.Termination.Lexicographic |
| 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 |
| readTextFile | Agda.Utils.IO.UTF8 |
| reallyUnLevelView | Agda.TypeChecking.Level |
| reason | Agda.Utils.QuickCheck |
| rebindClause | Agda.TypeChecking.Rebind |
| rebindPrimitive | Agda.TypeChecking.Primitive |
| 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 |
| recArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| RecBehaviour | Agda.Termination.Lexicographic |
| recBehaviourInvariant | Agda.Termination.Lexicographic |
| reccalc | Agda.Auto.NarrowingSearch |
| recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recCon | 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 |
| 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 |
| recordModule | Agda.TypeChecking.Records |
| RecordModuleIFS | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Records | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| RecordSig | Agda.Syntax.Concrete |
| recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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.Syntax.Concrete.Operators.Parser |
| redBind | Agda.TypeChecking.Primitive |
| redReturn | Agda.TypeChecking.Primitive |
| Reduce | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| reduce | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| reduceB | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| reduceCon | Agda.TypeChecking.Rules.Term |
| 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 |
| reduceHead | Agda.TypeChecking.Injectivity |
| RefCreateEnv | Agda.Auto.NarrowingSearch |
| Refinable | Agda.Auto.NarrowingSearch |
| 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 |
| refreshStr | Agda.Interaction.GhciTop |
| Reify | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reify | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyApp | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyDisplayForm | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyDisplayFormP | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyPatterns | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| Rel | |
| 1 (Data Constructor) | Agda.Compiler.Epic.Interface |
| 2 (Type/Class) | Agda.TypeChecking.Primitive |
| RelativeTo | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Relevance | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Compiler.Epic.Interface |
| 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 |
| relevantVars | Agda.TypeChecking.Free |
| relOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| remAbs | Agda.Compiler.Epic.Injection |
| remForced | Agda.Compiler.Epic.Forcing |
| removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| removeOnlyQualified | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| removeUnused | Agda.Compiler.Epic.Erasure |
| removevar | Agda.Auto.CaseSplit |
| Ren | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| ren | Agda.Auto.CaseSplit |
| rename | |
| 1 (Function) | Agda.Auto.CaseSplit |
| 2 (Function) | Agda.TypeChecking.Substitute |
| renameCanonicalNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| renameFrom | Agda.TypeChecking.Substitute |
| 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, Agda.Interaction.GhciTop |
| 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 |
| replaceForced | Agda.Compiler.Epic.Forcing |
| replaceFunCC | Agda.Compiler.Epic.Injection |
| replacep | Agda.Auto.CaseSplit |
| replay | Agda.Utils.QuickCheck |
| report | Agda.Compiler.Epic.Forcing |
| reportPostponing | Agda.TypeChecking.Rules.LHS.Unify |
| reportS | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| reportSDoc | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| reportSLn | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| requireLevels | Agda.TypeChecking.Level |
| 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, Agda.Interaction.GhciTop |
| resolveModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| resolveName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| Restore | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| restrictPrivate | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Result | |
| 1 (Type/Class) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Termination.TermCheck |
| retryConstraints | Agda.Interaction.CommandLine.CommandLine |
| Return | Agda.Interaction.CommandLine.CommandLine |
| returnBlock | Agda.Compiler.JS.Parser |
| reverseCCBody | Agda.Compiler.Epic.FromAgda |
| reverseP | Agda.Utils.Permutation |
| Rewrite | Agda.Interaction.BasicOps |
| rewrite | Agda.Interaction.BasicOps |
| RewriteRHS | Agda.Syntax.Abstract |
| RHS | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 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 |
| RightHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| rightHH | Agda.TypeChecking.Rules.LHS.Unify |
| RightOperandCtx | Agda.Syntax.Fixity |
| Rigid | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Data Constructor) | Agda.Utils.Warshall |
| 3 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| 4 (Data Constructor) | Agda.TypeChecking.SizedTypes |
| RigidId | Agda.Utils.Warshall |
| rigidVars | Agda.TypeChecking.Free |
| RIInferredTypeUnknown | Agda.Auto.Syntax |
| RIIotaStep | Agda.Auto.Syntax |
| RIMainInfo | 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 |
| roundFixBrackets | Agda.Syntax.Fixity |
| row | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| rowdescr | Agda.Utils.Warshall |
| rows | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| rparen | Agda.Utils.Pretty |
| rStart | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 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, Agda.Interaction.GhciTop |
| runAgda | Agda.Main |
| runExceptionT | Agda.TypeChecking.Monad.Exception |
| runIM | Agda.Interaction.Monad |
| runLookAhead | Agda.Syntax.Parser.LookAhead |
| runNice | Agda.Syntax.Concrete.Definitions |
| runTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| runTCM' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| runTests | Agda.Utils.TestHelpers |
| runUndo | Agda.Auto.NarrowingSearch |
| RVar | Agda.Utils.Warshall |