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 |