Agda-2.6.2.2: 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 |
1 (Data Constructor) | Agda.Auto.Options
2 (Type/Class) | Agda.TypeChecking.Serialise.Base
raise | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseErrors | Agda.Interaction.Library.Base
raiseErrors' | Agda.Interaction.Library.Base
raiseExeNotExecutable | Agda.TypeChecking.Unquote
raiseExeNotFound | Agda.TypeChecking.Unquote
raiseExeNotTrusted | Agda.TypeChecking.Unquote
raiseFrom | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
raiseFromS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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.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 | 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
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
rangesToPositions | Agda.Interaction.Highlighting.Range
rangeToInterval | Agda.Syntax.Position
rangeToIntervalWithFile | Agda.Syntax.Position
rangeToPositions | Agda.Interaction.Highlighting.Range
rangeToRange | Agda.Interaction.Highlighting.Range
rational | Agda.Utils.Pretty
ratioToDouble | Agda.Utils.Float
RawApp | Agda.Syntax.Concrete
rawApp | Agda.Syntax.Concrete
RawAppP | Agda.Syntax.Concrete
rawAppP | Agda.Syntax.Concrete
RawName | Agda.Syntax.Common
rawNameToString | Agda.Syntax.Common
rawValue | Agda.Auto.Syntax
rbrace | Agda.Utils.Pretty
rbrack | Agda.Utils.Pretty
RConst | Agda.Utils.Warshall
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
readFile | Agda.Utils.IO.UTF8
ReadFileError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
readFilePM | Agda.Syntax.Parser
readFromCachedLog | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
ReadGHCModuleEnv | Agda.Compiler.MAlonzo.Misc
ReadGHCOpts | Agda.Compiler.MAlonzo.Compiler
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.Compiler.Backend, Agda.TypeChecking.Monad
readTextFile | Agda.Utils.IO.UTF8
reallyAllReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReallyDontExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reallyDontExpandLast | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
reallyFree | Agda.TypeChecking.Rewriting.NonLinMatch
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.Compiler.Backend, Agda.TypeChecking.Monad
recalc | Agda.Auto.NarrowingSearch
recalcs | Agda.Auto.NarrowingSearch
reccalc | Agda.Auto.NarrowingSearch
RecCheck | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
recClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recComp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recConHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recConstructor | Agda.Syntax.Common
RecDef | Agda.Syntax.Abstract
recEtaEquality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recEtaEquality' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recFields | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recHasEta | Agda.Syntax.Common
recheckAbstractClause | Agda.Interaction.MakeCase
recInduction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recInductive | Agda.Syntax.Common
recMutual | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecName |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor) | Agda.Syntax.Scope.Base
recNamedCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Recompile |
1 (Type/Class) | Agda.Compiler.Backend
2 (Data Constructor) | Agda.Compiler.Backend
recomputeInScopeSets | Agda.Syntax.Scope.Base
recomputeInverseScopeMaps | Agda.Syntax.Scope.Base
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.Concrete
4 (Data Constructor) | Agda.Interaction.Highlighting.Precise
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecordAssign | Agda.Syntax.Abstract
RecordAssignment | Agda.Syntax.Concrete
RecordAssignments | Agda.Syntax.Concrete
RecordAssigns | Agda.Syntax.Abstract
RecordCon | Agda.TypeChecking.Datatypes
RecordDef |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Reflected
RecordDirective |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | 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.Rules.LHS
recordFieldNames | Agda.TypeChecking.Records
RecordFieldWarning |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recordFieldWarningToError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecordFlex | Agda.TypeChecking.Rules.LHS.Problem
recordInduction | Agda.TypeChecking.Rules.LHS
RecordModuleInstance |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recordPatternToProjections | Agda.TypeChecking.RecordPatterns
Records | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
RecordSig | Agda.Syntax.Concrete
recoverAsPatterns | Agda.Compiler.Treeless.AsPatterns
RecP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recPattern | Agda.Syntax.Common
recPatternMatching | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
recRecursive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RecSig | Agda.Syntax.Abstract
recTel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
RecursiveReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redBind | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redoChecks | Agda.Interaction.BasicOps
redReturn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
redSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Reduce |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class) | Agda.TypeChecking.Reduce
reduce | Agda.TypeChecking.Reduce
reduce' | Agda.TypeChecking.Reduce
reduceAllDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceDefCopy | Agda.TypeChecking.Reduce
reduceDefCopyTCM | Agda.TypeChecking.Reduce
ReduceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReduceEnv |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceHead | Agda.TypeChecking.Reduce
reduceIApply | Agda.TypeChecking.Reduce
reduceIApply' | Agda.TypeChecking.Reduce
ReduceM |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceProjectionLike | Agda.TypeChecking.ProjectionLike
reduceQuotedTerm | Agda.TypeChecking.Unquote
reduceSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reduceWithBlocker | Agda.TypeChecking.Reduce
RefCreateEnv |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
Refinable | Agda.Auto.NarrowingSearch
Refine | Agda.Interaction.InteractionTop
refine | Agda.Interaction.BasicOps
Refinement | Agda.Auto.Auto
refinements | Agda.Auto.NarrowingSearch
RefInfo | Agda.Auto.Syntax
reflClos | Agda.TypeChecking.SizedTypes.WarshallSolver
Reflected | Agda.Syntax.Common
registerInteractionPoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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
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.Compiler.Backend, Agda.TypeChecking.Monad
Relevant | Agda.Syntax.Common
relevantIn | Agda.TypeChecking.Free
relevantInIgnoringSortAnn | Agda.TypeChecking.Free
relOfConst | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
Remove |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
removeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional
RemoveHighlighting | Agda.Interaction.Response
removeInteractionPoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
RemoveTokenBasedHighlighting | Agda.Interaction.Response
removevar | Agda.Auto.CaseSplit
Ren | Agda.Syntax.Abstract
ren | Agda.Auto.CaseSplit
rename | Agda.Auto.Syntax
renameCanonicalNames | Agda.Syntax.Scope.Base
renameNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
renameNodesMonotonic | Agda.Utils.Graph.AdjacencyMap.Unidirectional
renameOffset | Agda.Auto.Syntax
renameP | Agda.TypeChecking.Substitute
renameTel | Agda.TypeChecking.Telescope
Renaming |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Concrete
4 (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.Utils.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
renderStyle | Agda.Utils.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
RepeatedVariablesInPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
repeatWhile | Agda.Utils.Function
repeatWhileM | Agda.Utils.Function
repl |
1 (Function) | Agda.Compiler.Common
2 (Function) | Agda.Interaction.AgdaTop
Replace | Agda.Auto.CaseSplit
replace | Agda.Auto.CaseSplit
replace' | Agda.Auto.CaseSplit
replaceEmptyName | Agda.Syntax.Internal
replacementChar | Agda.Utils.Char
replaceModuleExtension | Agda.Interaction.FindFile
replacep | Agda.Auto.CaseSplit
replaceSurrogateCodePoint | Agda.Utils.Char
ReplaceWith | Agda.Auto.CaseSplit
replInteractor | Agda.Main
reportResult | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReportS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reportS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reportSDoc | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reportSLn | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ReqArg | Agda.Interaction.Options
requireAllowExec | Agda.TypeChecking.Unquote
requireCubical | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
requireGuarded | Agda.TypeChecking.Lock
requireLevels | Agda.TypeChecking.Level
requireOptionRewriting | Agda.TypeChecking.Rewriting
Res | Agda.TypeChecking.MetaVars
reset | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
resetAllState | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
resetLayoutStatus | Agda.Syntax.Parser.Monad
resetState | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
resolvedBindingSource | Agda.Syntax.Scope.Base
ResolvedName | Agda.Syntax.Scope.Base
resolvedVar | Agda.Syntax.Scope.Base
resolveModule | Agda.Syntax.Scope.Monad
resolveName | Agda.Syntax.Scope.Monad
resolveName' | Agda.Syntax.Scope.Monad
resolveUnknownInstanceDefs | Agda.TypeChecking.Telescope
respInScope | Agda.Interaction.Response
respLetValue | Agda.Interaction.Response
Response | Agda.Interaction.Response
response | Agda.Interaction.EmacsCommand
ResponseContextEntry |
1 (Type/Class) | Agda.Interaction.Response
2 (Data Constructor) | Agda.Interaction.Response
respOrigName | Agda.Interaction.Response
respReifName | Agda.Interaction.Response
respType | Agda.Interaction.Response
Resp_ClearHighlighting | Agda.Interaction.Response
Resp_ClearRunningInfo | Agda.Interaction.Response
Resp_DisplayInfo | Agda.Interaction.Response
Resp_DoneAborting | Agda.Interaction.Response
Resp_DoneExiting | 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
restartOptions | Agda.Interaction.Options
Restore |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
restorePostScopeState | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
restrictLocalPrivate | Agda.Syntax.Scope.Base
restrictPrivate | Agda.Syntax.Scope.Base
restrictTo | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
Result | Agda.Termination.TermCheck
returnExpr | Agda.Syntax.Concrete
returnTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
reverse | Agda.Utils.List1
ReversedSuffix | Agda.Utils.List
reverseP | Agda.Utils.Permutation
revisitRecordPatternTranslation | Agda.TypeChecking.Rules.Decl
revLift | Agda.Interaction.InteractionTop
revLiftTC | Agda.Interaction.InteractionTop
rewContext | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewFromClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewPats | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewRHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Rewrite |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Interaction.Base
rewrite | Agda.TypeChecking.Rewriting
RewriteAmbiguousRules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteAmbiguousRules_ | 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
RewriteMaybeNonConfluent | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteMaybeNonConfluent_ | Agda.Interaction.Options.Warnings
RewriteMissingRule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteMissingRule_ | Agda.Interaction.Options.Warnings
RewriteNonConfluent | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteNonConfluent_ | Agda.Interaction.Options.Warnings
RewritePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
RewriteRHS | Agda.Syntax.Abstract
rewriteRHS | Agda.Syntax.Abstract
RewriteRule |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteRuleMap | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
RewriteRules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
rewriteStrippedPats | Agda.Syntax.Abstract
rewriteWhereDecls | Agda.Syntax.Abstract
rewriteWith | Agda.TypeChecking.Rewriting
rewType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, 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.Utils.Haskell.Syntax
RHS' | Agda.Syntax.Concrete
rhsConcrete | Agda.Syntax.Abstract
rhsExpr | 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.Common
RightDisjunct | Agda.Auto.NarrowingSearch
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 (Type/Class) | Agda.Utils.Warshall
4 (Data Constructor) | Agda.Utils.Warshall
5 (Data Constructor) | Agda.TypeChecking.SizedTypes
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
rigidName | Agda.TypeChecking.SizedTypes.Solve
RigidOf | Agda.TypeChecking.SizedTypes.Syntax
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
RLiteral | Agda.Syntax.Literal
rm | Agda.Auto.NarrowingSearch
rollback | Agda.Syntax.Parser.LookAhead
RollBackMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
rootNameModule | Agda.Interaction.FindFile
roundFixBrackets | Agda.Syntax.Fixity
row | Agda.Termination.SparseMatrix
rowdescr | Agda.Utils.Warshall
rows | Agda.Termination.SparseMatrix
rparen | Agda.Utils.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
runAbsToCon | Agda.Syntax.Translation.AbstractToConcrete
runAgda | Agda.Main
runAgda' | Agda.Main
runAgdaWithOptions | Agda.Main
runBlocked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
runListT | Agda.Utils.ListT
runLookAhead | Agda.Syntax.Parser.LookAhead
RunMetaOccursCheck |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Warnings
runPMIO | Agda.Syntax.Parser
runPureConversion | Agda.TypeChecking.Conversion.Pure
RunRecordPatternTranslation |
1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile
runReduceF | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runReduceM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runRefCreateEnv | Agda.Auto.NarrowingSearch
runSafeTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runStConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTCMPrettyErrors | Agda.Main
runTCMTop | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTCMTop' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
runTer | Agda.Termination.Monad
runTerDefault | Agda.Termination.Monad
runUndo | Agda.Auto.NarrowingSearch
runUnquoteM | Agda.TypeChecking.Unquote
runUpdater | Agda.Utils.Update
runUpdaterT | Agda.Utils.Update
RVar | Agda.Utils.Warshall