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

- 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
raise | Agda.TypeChecking.Substitute
raiseFrom | Agda.TypeChecking.Substitute
raiseFromCC | Agda.Compiler.Epic.Forcing
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
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
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
Records | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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 | 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.Erasure
2 (Type/Class) | Agda.TypeChecking.Primitive
RelativeTo | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Relevance | Agda.Syntax.Common
relevancies | Agda.Compiler.Epic.Erasure
Relevancy | Agda.Compiler.Epic.Erasure
Relevant | Agda.Syntax.Common
relevant | Agda.Compiler.Epic.Erasure
relOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
remForced | Agda.Compiler.Epic.Forcing
removeForced | Agda.Compiler.Epic.Forcing
removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
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.Telescope
renameCanonicalNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
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
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
replacep | Agda.Auto.CaseSplit
replay | Agda.Utils.QuickCheck
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
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
response | 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
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
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
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