Agda-2.8.0: 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.TypeChecking.Serialise.Base
raise | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseErrors | Agda.Interaction.Library.Base
raiseErrors' | Agda.Interaction.Library.Base
raiseFrom | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseFromS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseNonFatalErrors | Agda.Interaction.Imports
raiseS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseWarningsOnUsage | Agda.TypeChecking.Warnings
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.Utils.IArray
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
RangeFile |
1 (Type/Class) | Agda.Syntax.Position
2 (Data Constructor) | Agda.Syntax.Position
rangeFile | Agda.Syntax.Position
rangeFileName | Agda.Syntax.Position
rangeFilePath | Agda.Syntax.Position
rangeFromAbsolutePath | Agda.Syntax.Position
rangeIntervals | Agda.Syntax.Position
rangeInvariant |
1 (Function) | Agda.Syntax.Position
2 (Function) | Agda.Interaction.Highlighting.Range
RangeMap |
1 (Type/Class) | Agda.Utils.RangeMap
2 (Data Constructor) | Agda.Utils.RangeMap
rangeMap | Agda.Utils.RangeMap
rangeMapInvariant | Agda.Utils.RangeMap
rangeModule | Agda.Syntax.Position
rangeModule' | Agda.Syntax.Position
rangeOf | Agda.Syntax.Common
RangePair |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
rangePair | Agda.Interaction.Highlighting.Precise
rangePairInvariant | Agda.Interaction.Highlighting.Precise
Ranges |
1 (Type/Class) | Agda.Interaction.Highlighting.Range
2 (Data Constructor) | Agda.Interaction.Highlighting.Range
rangesInvariant | Agda.Interaction.Highlighting.Range
rangeSize | Agda.Utils.IArray
rangesToPositions | Agda.Interaction.Highlighting.Range
rangeToInterval | Agda.Syntax.Position
rangeToIntervalWithFile | Agda.Syntax.Position
rangeToPositions | Agda.Interaction.Highlighting.Range
rangeToRange | Agda.Interaction.Highlighting.Range
RangeWithoutFile | Agda.Syntax.Position
rational | Agda.Syntax.Common.Pretty
ratioToDouble | Agda.Utils.Float
RawApp | Agda.Syntax.Concrete
rawApp | Agda.Syntax.Concrete
RawAppP | Agda.Syntax.Concrete
rawAppP | Agda.Syntax.Concrete
rawModuleNameInferred | Agda.Syntax.TopLevelModuleName
rawModuleNameParts | Agda.Syntax.TopLevelModuleName
rawModuleNameRange | Agda.Syntax.TopLevelModuleName
RawName | Agda.Syntax.Common
rawNameToString | Agda.Syntax.Common
RawTopLevelModuleName |
1 (Type/Class) | Agda.Syntax.TopLevelModuleName
2 (Data Constructor) | Agda.Syntax.TopLevelModuleName
rawTopLevelModuleName | Agda.Syntax.TopLevelModuleName
rawTopLevelModuleNameForModule | Agda.Syntax.TopLevelModuleName
rawTopLevelModuleNameForModuleName | Agda.Syntax.TopLevelModuleName
rawTopLevelModuleNameForQName | Agda.Syntax.TopLevelModuleName
rawTopLevelModuleNameToString | Agda.Syntax.TopLevelModuleName
rbrace | Agda.Syntax.Common.Pretty
rbrack | Agda.Syntax.Common.Pretty
reAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
reachable | Agda.Utils.Graph.AdjacencyMap.Unidirectional
reachableFrom | Agda.Utils.Graph.AdjacencyMap.Unidirectional
reachableFromSet | Agda.Utils.Graph.AdjacencyMap.Unidirectional
readBinaryFile' | Agda.Utils.IO.Binary
readdTypedInstance | Agda.TypeChecking.InstanceArguments
ReadError | Agda.Interaction.Library.Base
ReadException | Agda.Utils.IO.UTF8
ReadFailure | Agda.Interaction.Library.Base
readFile | Agda.Utils.IO.UTF8
ReadFileError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
readFilePM | Agda.Syntax.Parser
readFromCachedLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReadGHCModuleEnv | Agda.Compiler.MAlonzo.Misc
readInterface | Agda.Interaction.Imports
readIORef | Agda.Utils.IORef
readline | Agda.Interaction.Monad
readModifyIORef' | Agda.Utils.IORef
readParse | Agda.Interaction.Base
readsToParse | Agda.Interaction.Base
ReadTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
readTextFile | Agda.Utils.IO.UTF8
readTokens | Agda.Mimer.Options
reallyAllReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReallyDontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reallyDontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reallyFree | Agda.TypeChecking.Free.Reduce
reallyNoConstraints | Agda.TypeChecking.Constraints
ReallyNotBlocked | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
reallyNotFreeIn | Agda.TypeChecking.MetaVars.Occurs
reallyUnLevelView | Agda.TypeChecking.Level
rebindName | Agda.Syntax.Scope.Monad
Rec |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecCheck | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recConstructor | Agda.Syntax.Common
RecDef | Agda.Syntax.Abstract
RecDefS | Agda.Syntax.Abstract
recEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recEtaEquality' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recHasEta | Agda.Syntax.Common
recheckAbstractClause | Agda.Interaction.MakeCase
recheckBecausePragmaOptionsChanged | Agda.Interaction.Options
recInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recInductive | Agda.Syntax.Common
recMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecName |
1 (Data Constructor) | Agda.Syntax.Scope.Base
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
recNamedCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecName_ | Agda.Interaction.Options.Errors
Recompile |
1 (Type/Class) | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
recomputeInScopeSets | Agda.Syntax.Scope.Base
recomputeInverseScopeMaps | Agda.Syntax.Scope.Base
reconstruct | Agda.TypeChecking.ReconstructParameters
reconstructAction | Agda.TypeChecking.ReconstructParameters
reconstructAction' | Agda.TypeChecking.ReconstructParameters
reconstructParameters | Agda.TypeChecking.ReconstructParameters
reconstructParameters' | Agda.TypeChecking.ReconstructParameters
reconstructParametersInEqView | Agda.TypeChecking.ReconstructParameters
reconstructParametersInTel | Agda.TypeChecking.ReconstructParameters
reconstructParametersInType | Agda.TypeChecking.ReconstructParameters
reconstructParametersInType' | Agda.TypeChecking.ReconstructParameters
Record |
1 (Type/Class) | Agda.Utils.Lens.Examples
2 (Data Constructor) | Agda.Utils.Lens.Examples
3 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
4 (Data Constructor) | Agda.Syntax.Concrete
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordAssign | Agda.Syntax.Abstract
RecordAssignment | Agda.Syntax.Concrete
RecordAssignments | Agda.Syntax.Concrete
RecordAssigns | Agda.Syntax.Abstract
RecordCon | Agda.TypeChecking.Datatypes
RecordConName | Agda.Syntax.Abstract
recordConName | Agda.Syntax.Abstract
RecordData |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordDef |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete
RecordDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordDirective | Agda.Syntax.Concrete
RecordDirectives |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
RecordDirectives' | Agda.Syntax.Common
recordEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recordFieldNames | Agda.TypeChecking.Records
RecordFieldWarning |
1 (Type/Class) | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recordFieldWarningToError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordFlex | Agda.TypeChecking.Rules.LHS.Problem
recordInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordIsErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordIsErased_ | Agda.Interaction.Options.Errors
RecordModuleInstance |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recordPatternToProjections | Agda.TypeChecking.RecordPatterns
recordRHSToCopatterns | Agda.TypeChecking.RecordPatterns
Records | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecordSig | Agda.Syntax.Concrete
recoverAsPatterns | Agda.Compiler.Treeless.AsPatterns
recoverLayout | Agda.Syntax.Parser.Helpers
RecP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recPattern | Agda.Syntax.Common
recPatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recRecursive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recRecursive_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecSig | Agda.Syntax.Abstract
RecSigS | Agda.Syntax.Abstract
recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
recTerminates | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecUpdate |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recurseExpr | Agda.Syntax.Abstract.Views
RecurseExprFn | Agda.Syntax.Abstract.Views
RecurseExprRecFn | Agda.Syntax.Abstract.Views
recursive | Agda.Termination.RecCheck
recursiveRecord | Agda.TypeChecking.Records
RecursiveRecordNeedsInductivity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RecursiveRecordNeedsInductivity_ | Agda.Interaction.Options.Errors
RecursiveReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redBind | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redoChecks | Agda.Interaction.BasicOps
redPred | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redReturn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
redReturnNoSimpl | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
redSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Reduce |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class) | Agda.TypeChecking.Reduce
reduce | Agda.TypeChecking.Reduce
reduce' | Agda.TypeChecking.Reduce
reduce2Lam | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
reduceAllDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReduceAndEtaContract | Agda.TypeChecking.MetaVars
reduceAndEtaContract | Agda.TypeChecking.MetaVars
reduceB | Agda.TypeChecking.Reduce
reduceB' | Agda.TypeChecking.Reduce
Reduced |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceDefCopy | Agda.TypeChecking.Reduce
reduceDefCopyTCM | Agda.TypeChecking.Reduce
ReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReduceEnv |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceHead | Agda.TypeChecking.Reduce
reduceIApply' | Agda.TypeChecking.Reduce
ReduceM |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceProjectionLike | Agda.TypeChecking.ProjectionLike
reduceQuotedTerm | Agda.TypeChecking.Unquote
reduceSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reduceWithBlocker | Agda.TypeChecking.Reduce
ReferencesFutureVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReferencesFutureVariables_ | Agda.Interaction.Options.Errors
Refine | Agda.Interaction.InteractionTop
refine | Agda.Interaction.BasicOps
reflClos | Agda.TypeChecking.SizedTypes.WarshallSolver
Reflected | Agda.Syntax.Common
Reflection | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
registerFileId | Agda.Utils.FileId
registerFileId' | Agda.Utils.FileId
registerFileId'' | Agda.Utils.FileId
registerFileIdWithBuiltin | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
registerInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReifiesTo | Agda.Syntax.Translation.InternalToAbstract
Reify | Agda.Syntax.Translation.InternalToAbstract
reify | Agda.Syntax.Translation.InternalToAbstract
reifyDisplayFormP | Agda.Syntax.Translation.InternalToAbstract
reifyElimToExpr | Agda.Interaction.BasicOps
reifyPatterns | Agda.Syntax.Translation.InternalToAbstract
reifyUnblocked | Agda.Syntax.Translation.InternalToAbstract
reifyWhen | Agda.Syntax.Translation.InternalToAbstract
reintroduceEllipsis | Agda.Syntax.Concrete.Pattern
rejectUnknownFields | Agda.Interaction.JSON
Rel | Agda.TypeChecking.Primitive
Related | Agda.Syntax.Common
related | Agda.Utils.PartialOrd
relativizeAbsolutePath | Agda.Utils.FileName
Relevance | Agda.Syntax.Common
RelevanceAttribute | Agda.Syntax.Concrete.Attribute
relevanceAttributes | Agda.Syntax.Concrete.Attribute
relevanceAttributeTable | Agda.Syntax.Concrete.Attribute
RelevanceMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RelevanceMismatch_ | Agda.Interaction.Options.Errors
Relevant | Agda.Syntax.Common
relevant | Agda.Syntax.Common
relevantIn | Agda.TypeChecking.Free
relevantInIgnoringSortAnn | Agda.TypeChecking.Free
relOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
relToDontCare | Agda.TypeChecking.Substitute
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
RemoteMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RemoteMetaVariable |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Remove |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
removeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional
RemoveHighlighting | Agda.Interaction.Response.Base, Agda.Interaction.Response
removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
removeLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
removeLetBindingsFrom | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
removeLoneSig | Agda.Syntax.Concrete.Definitions.Monad
removeNameFromScope | Agda.Syntax.Scope.Base
removeNode | Agda.Utils.Graph.AdjacencyMap.Unidirectional
removeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
removeOldInteractionScope | Agda.Interaction.InteractionTop
removeParenP | Agda.Syntax.Concrete
removeSucs | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RemoveTokenBasedHighlighting | Agda.Interaction.Response.Base, Agda.Interaction.Response
Ren | Agda.Syntax.Abstract
renameCanonicalNames | Agda.Syntax.Scope.Base
renameNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
renameNodesMonotonic | Agda.Utils.Graph.AdjacencyMap.Unidirectional
renameP | Agda.TypeChecking.Substitute
renameTel | Agda.TypeChecking.Telescope
Renaming |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
renaming | Agda.TypeChecking.Substitute
Renaming' | Agda.Syntax.Common
RenamingDirective | Agda.Syntax.Concrete
RenamingDirective' | Agda.Syntax.Common
renamingR | Agda.TypeChecking.Substitute
rEnd | Agda.Syntax.Position
rEnd' | Agda.Syntax.Position
render |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
renderAnsiIO | Agda.Syntax.Common.Pretty.ANSI
renderDot | Agda.Interaction.Highlighting.Dot.Base
renderDotToFile | Agda.Interaction.Highlighting.Dot.Base
renderError | Agda.TypeChecking.Errors
renderErrorParts | Agda.TypeChecking.Unquote
renderSpans | Agda.Syntax.Common.Pretty
renderStyle | Agda.Syntax.Common.Pretty
renderSuffix | Agda.Utils.Suffix
renFixity | Agda.Syntax.Common
renFrom | Agda.Syntax.Common
renModules | Agda.Syntax.Abstract
renNames | Agda.Syntax.Abstract
renTo | Agda.Syntax.Common
renToRange | Agda.Syntax.Common
reorder | Agda.Compiler.JS.Compiler
reorder' | Agda.Compiler.JS.Compiler
reorderTel | Agda.TypeChecking.Telescope
reorderTel_ | Agda.TypeChecking.Telescope
repeat | Agda.Utils.List1
RepeatedNamesInImportDirective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RepeatedNamesInImportDirective_ | Agda.Interaction.Options.Errors
RepeatedVariablesInPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RepeatedVariablesInPattern_ | Agda.Interaction.Options.Errors
repeatWhile | Agda.Utils.Function
repeatWhileM | Agda.Utils.Function
repl |
1 (Function) | Agda.Compiler.Common
2 (Function) | Agda.Interaction.AgdaTop
replaceEmptyName | Agda.Syntax.Internal
replacementChar | Agda.Utils.Char
replaceModuleExtension | Agda.Interaction.FindFile
replaceSurrogateCodePoint | Agda.Utils.Char
replInteractor | Agda.Main
reportResult | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReportS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reportS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reportSDoc | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reportSLn | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ReqArg | Agda.Utils.GetOpt, Agda.Interaction.Options
requireAllowExec | Agda.TypeChecking.Unquote
requireCubical | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
requireLevels | Agda.TypeChecking.Level
requireOptionRewriting | Agda.TypeChecking.Rewriting
requireOptionSizedTypes | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RequireOrder | Agda.Utils.GetOpt
RequiresDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Res | Agda.TypeChecking.MetaVars
reset | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
resetAllState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
resetLayoutStatus | Agda.Syntax.Parser.Monad
resetState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
resolvedBindingSource | Agda.Syntax.Scope.Base
ResolvedName | Agda.Syntax.Scope.Base
resolvedVar | Agda.Syntax.Scope.Base
ResolveInstanceHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
resolveInstanceHead | Agda.TypeChecking.InstanceArguments
ResolveInstanceOF | Agda.Interaction.Base
resolveModule | Agda.Syntax.Scope.Monad
resolveName | Agda.Syntax.Scope.Monad
resolveName' | Agda.Syntax.Scope.Monad
respInScope | Agda.Interaction.Response.Base, Agda.Interaction.Response
respLetValue | Agda.Interaction.Response.Base, Agda.Interaction.Response
Response | Agda.Interaction.Response
response | Agda.Interaction.EmacsCommand
ResponseContextEntry |
1 (Type/Class) | Agda.Interaction.Response.Base, Agda.Interaction.Response
2 (Data Constructor) | Agda.Interaction.Response.Base, Agda.Interaction.Response
Response_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response
respOrigName | Agda.Interaction.Response.Base, Agda.Interaction.Response
respReifName | Agda.Interaction.Response.Base, Agda.Interaction.Response
respType | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_ClearHighlighting | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_ClearRunningInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_DisplayInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_DoneAborting | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_DoneExiting | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_GiveAction | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_HighlightingInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_InteractionPoints | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_JumpToError | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_MakeCase | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_Mimer | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_RunningInfo | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_SolveAll | Agda.Interaction.Response.Base, Agda.Interaction.Response
Resp_Status | Agda.Interaction.Response.Base, Agda.Interaction.Response
restorePostScopeState | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
restrictKeys | Agda.Utils.Map1
restrictLocalPrivate | Agda.Syntax.Scope.Base
restrictPrivate | Agda.Syntax.Scope.Base
restrictTo | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
Result | Agda.Termination.TermCheck
resultBlocker | Agda.TypeChecking.DiscrimTree
resultValues | Agda.TypeChecking.DiscrimTree
Retract | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
returnExpr | Agda.Syntax.Concrete
ReturnInOrder | Agda.Utils.GetOpt
returnTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
reverse | Agda.Utils.List1
ReversedSuffix | Agda.Utils.List
reverseP | Agda.Utils.Permutation
revisitRecordPatternTranslation | Agda.TypeChecking.Rules.Decl
revLift | Agda.Interaction.Command
revLiftTC | Agda.Interaction.Command
rewContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewFromClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Rewrite |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Interaction.Base
rewrite | Agda.TypeChecking.Rewriting
RewriteAmbiguousRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteAmbiguousRules_ | Agda.Interaction.Options.Warnings
RewriteBeforeFunctionDefinition_ | Agda.Interaction.Options.Warnings
RewriteBeforeMutualFunctionDefinition_ | Agda.Interaction.Options.Warnings
RewriteBlockedOnProblems_ | Agda.Interaction.Options.Warnings
RewriteConstructorParametersNotGeneral_ | Agda.Interaction.Options.Warnings
RewriteContainsUnsolvedMetaVariables_ | Agda.Interaction.Options.Warnings
RewriteDoesNotTargetRewriteRelation_ | Agda.Interaction.Options.Warnings
RewriteEqn |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
RewriteEqn' | Agda.Syntax.Common
rewriteExprs | Agda.Syntax.Abstract
RewriteHeadSymbolContainsMetas_ | Agda.Interaction.Options.Warnings
RewriteHeadSymbolIsProjectionLikeFunction_ | Agda.Interaction.Options.Warnings
RewriteHeadSymbolIsTypeConstructor_ | Agda.Interaction.Options.Warnings
RewriteLHSNotDefinitionOrConstructor_ | Agda.Interaction.Options.Warnings
RewriteLHSReduces_ | Agda.Interaction.Options.Warnings
RewriteMaybeNonConfluent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteMaybeNonConfluent_ | Agda.Interaction.Options.Warnings
RewriteMissingRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteMissingRule_ | Agda.Interaction.Options.Warnings
RewriteNonConfluent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteNonConfluent_ | Agda.Interaction.Options.Warnings
RewritePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
rewriteRelationDom | Agda.TypeChecking.Rewriting
RewriteRequiresDefinitions_ | Agda.Interaction.Options.Warnings
RewriteRHS | Agda.Syntax.Abstract
rewriteRHS | Agda.Syntax.Abstract
RewriteRHSS | Agda.Syntax.Abstract
RewriteRule |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteRuleMap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewritesNothing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
RewritesNothing_ | Agda.Interaction.Options.Warnings
rewriteStrippedPats | Agda.Syntax.Abstract
RewriteVariablesBoundMoreThanOnce_ | Agda.Interaction.Options.Warnings
RewriteVariablesNotBoundByLHS_ | Agda.Interaction.Options.Warnings
rewriteWhereDecls | Agda.Syntax.Abstract
rewriteWith | Agda.TypeChecking.Rewriting
rewTopModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rewType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Utils.Haskell.Syntax
RHS' | Agda.Syntax.Concrete
rhsConcrete | Agda.Syntax.Abstract
rhsExpr | Agda.Syntax.Abstract
RHSOrTypeSigs | Agda.Syntax.Parser.Helpers
RHSS | Agda.Syntax.Abstract
RHSSpine | Agda.Syntax.Abstract
rhsSpine | Agda.Syntax.Abstract
ribbonsPerLine | Agda.Syntax.Common.Pretty
RightAssoc | Agda.Syntax.Common
rightExpr | Agda.TypeChecking.SizedTypes.Syntax
rightIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
rightMargin | Agda.Syntax.Position
RightOperandCtx | Agda.Syntax.Fixity
rights | Agda.Utils.List1
Rigid |
1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor) | Agda.TypeChecking.SizedTypes
rigid | Agda.TypeChecking.SizedTypes.Syntax
RigidId | Agda.TypeChecking.SizedTypes.Syntax
rigidId | Agda.TypeChecking.SizedTypes.Syntax
rigidIndex | Agda.TypeChecking.SizedTypes.Syntax
RigidK | Agda.TypeChecking.DiscrimTree.Types
rigidName | Agda.TypeChecking.SizedTypes.Syntax
RigidOf | Agda.TypeChecking.SizedTypes.Syntax
Rigids | Agda.TypeChecking.SizedTypes.Syntax
rigids | Agda.TypeChecking.SizedTypes.Syntax
rigidVars | Agda.TypeChecking.Free
rigidVarsNotContainedIn | Agda.TypeChecking.MetaVars.Occurs
RLiteral | Agda.Syntax.Literal
rmvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rmvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rmvModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rollback | Agda.Syntax.Parser.LookAhead
RollBackMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
rootNameModule | Agda.Interaction.FindFile
RootNameModuleNotAQualifiedModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
roundFixBrackets | Agda.Syntax.Fixity
row | Agda.Termination.SparseMatrix
rows | Agda.Termination.SparseMatrix
rparen | Agda.Syntax.Common.Pretty
rStart | Agda.Syntax.Position
rStart' | Agda.Syntax.Position
RstFileType | Agda.Syntax.Common
RString | Agda.Syntax.Common
rtmError | Agda.Compiler.MAlonzo.Misc
rtmHole | Agda.Compiler.MAlonzo.Misc
rtmQual | Agda.Compiler.MAlonzo.Misc
rtmUnreachableError | Agda.Compiler.MAlonzo.Misc
rtmVar | Agda.Compiler.MAlonzo.Misc
rToR | Agda.Interaction.Highlighting.Range
rtrim | Agda.Utils.String
runAgda | Agda.Main
runAgda' | Agda.Main
runAgdaWithOptions | Agda.Main
runBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runBuiltinAccess | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runChange | Agda.Utils.Update
runChangeT | Agda.Utils.Update
runFail | Agda.Utils.Fail
runFail_ | Agda.Utils.Fail
runFree | Agda.TypeChecking.Free
runFreeM | Agda.TypeChecking.Free.Lazy
runGetState | Agda.TypeChecking.Serialise.Base
runHighlighter | Agda.Interaction.Highlighting.FromAbstract
runHsCompileT | Agda.Compiler.MAlonzo.Misc
runHsCompileT' | Agda.Compiler.MAlonzo.Misc
runIM | Agda.Interaction.Monad
runInteraction | Agda.Interaction.InteractionTop
runInteractionLoop | Agda.Interaction.CommandLine
runLexAction | Agda.Syntax.Parser.Alex
runLibM | Agda.Interaction.Library.Base
runListT | Agda.Utils.ListT
runLogHtmlWith | Agda.Interaction.Highlighting.HTML.Base
runLookAhead | Agda.Syntax.Parser.LookAhead
RunMetaOccursCheck |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runMListT | Agda.Utils.ListT
runNames | Agda.TypeChecking.Names
runNamesT | Agda.TypeChecking.Names
runNice | Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
runNLM | Agda.TypeChecking.Rewriting.NonLinMatch
runOptM | Agda.Interaction.Options
runP | Agda.Interaction.Library.Parse
runPM | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runPMDropWarnings | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runPMIO | Agda.Syntax.Parser
runPureConversion | Agda.TypeChecking.Conversion.Pure
runPureConversionB | Agda.TypeChecking.Conversion.Pure
RunRecordPatternTranslation |
1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile
runReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runSafeTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runStConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTCMPrettyErrors | Agda.Main
runTCMTop | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTCMTop' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
runTer | Agda.Termination.Monad
runTerDefault | Agda.Termination.Monad
runUnifyLogT | Agda.TypeChecking.Rules.LHS.Unify.Types
runUnquoteM | Agda.TypeChecking.Unquote
runUpdater | Agda.Utils.Update
runUpdaterT | Agda.Utils.Update