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

Index - S

S 
1 (Data Constructor)Agda.Auto.Options
2 (Type/Class)Agda.TypeChecking.Serialise.Base
3 (Type/Class)Agda.Auto.Convert
4 (Data Constructor)Agda.Auto.Convert
safeButNotBuiltinAgda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
safeFlagAgda.Interaction.Options
SafeFlagEtaAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagEta_Agda.Interaction.Options.Warnings
SafeFlagInjectiveAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagInjective_Agda.Interaction.Options.Warnings
SafeFlagNoCoverageCheckAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNoCoverageCheck_Agda.Interaction.Options.Warnings
SafeFlagNonTerminatingAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNonTerminating_Agda.Interaction.Options.Warnings
SafeFlagNoPositivityCheckAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNoPositivityCheck_Agda.Interaction.Options.Warnings
SafeFlagNoUniverseCheckAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNoUniverseCheck_Agda.Interaction.Options.Warnings
SafeFlagPolarityAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagPolarity_Agda.Interaction.Options.Warnings
SafeFlagPostulateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagPostulate_Agda.Interaction.Options.Warnings
SafeFlagPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagPragma_Agda.Interaction.Options.Warnings
SafeFlagTerminatingAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagTerminating_Agda.Interaction.Options.Warnings
SafeFlagWithoutKFlagPrimEraseEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagWithoutKFlagPrimEraseEquality_Agda.Interaction.Options.Warnings
SafeModeAgda.Interaction.Options.Lenses
sameCohesionAgda.Syntax.Common
sameDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sameErasedAgda.Syntax.Common
sameFileAgda.Utils.FileName
sameHidingAgda.Syntax.Common
sameKindAgda.Syntax.Concrete.Definitions.Types
sameModalityAgda.Syntax.Common
sameNameAgda.Syntax.Common
sameQuantityAgda.Syntax.Common
sameRelevanceAgda.Syntax.Common
sameRoot 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
sameVarsAgda.TypeChecking.Conversion
sanityCheckPragmaAgda.Compiler.MAlonzo.Pragmas
sanityCheckSubstAgda.Syntax.Internal.SanityCheck
sanityCheckVarsAgda.Syntax.Internal.SanityCheck
sat 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Concrete.Operators.Parser.Monad
sat' 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Concrete.Operators.Parser.Monad
satNoPlaceholderAgda.Syntax.Concrete.Operators.Parser
saturateOpaqueBlocksAgda.TypeChecking.Opacity
sayWhenAgda.TypeChecking.Pretty.Call
sayWhereAgda.TypeChecking.Pretty.Call
SBoolAgda.Utils.TypeLits
scanlAgda.Utils.List1
scanl1Agda.Utils.List1
scanrAgda.Utils.List1
scanr1Agda.Utils.List1
scatterMPAgda.Utils.Monad
sccDAGAgda.Utils.Graph.AdjacencyMap.Unidirectional
sccDAG'Agda.Utils.Graph.AdjacencyMap.Unidirectional
scCheckpointsAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
sccomcountAgda.Auto.NarrowingSearch
sccsAgda.Utils.Graph.AdjacencyMap.Unidirectional
sccs'Agda.Utils.Graph.AdjacencyMap.Unidirectional
scflipAgda.Auto.NarrowingSearch
sCheckedAgda.Interaction.Response
SClauseAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
sConstsAgda.Auto.Convert
Scope 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
3 (Type/Class)Agda.Utils.Warshall
ScopeCheckAgda.Interaction.Imports
ScopeCheckDeclarationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ScopeCheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
scopeCheckImportAgda.Interaction.Imports
scopeCheckingSufficesAgda.Compiler.Backend
ScopeCheckLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ScopeCopyInfo 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
scopeCurrentAgda.Syntax.Scope.Base
scopeDatatypeModuleAgda.Syntax.Scope.Base
ScopedDeclAgda.Syntax.Abstract
ScopedDeclSAgda.Syntax.Abstract
ScopedExprAgda.Syntax.Abstract
scopedExprAgda.TypeChecking.Rules.Term
scopeFixitiesAgda.Syntax.Scope.Base
scopeFixitiesAndPolaritiesAgda.Syntax.Scope.Base
scopeImportsAgda.Syntax.Scope.Base
ScopeInfo 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
scopeInScopeAgda.Syntax.Scope.Base
scopeInverseModuleAgda.Syntax.Scope.Base
scopeInverseNameAgda.Syntax.Scope.Base
scopeLocalsAgda.Syntax.Scope.Base
scopeLookupAgda.Syntax.Scope.Base
scopeLookup'Agda.Syntax.Scope.Base
ScopeMAgda.Syntax.Scope.Monad
ScopeMemo 
1 (Type/Class)Agda.Syntax.Scope.Monad
2 (Data Constructor)Agda.Syntax.Scope.Monad
scopeModulesAgda.Syntax.Scope.Base
scopeNameAgda.Syntax.Scope.Base
scopeNameSpaceAgda.Syntax.Scope.Base
ScopeNameSpacesAgda.Syntax.Scope.Base
scopeNameSpacesAgda.Syntax.Scope.Base
scopeParentsAgda.Syntax.Scope.Base
scopePolaritiesAgda.Syntax.Scope.Base
scopePrecedenceAgda.Syntax.Scope.Base
scopeVarsToBindAgda.Syntax.Scope.Base
scopeWarningAgda.Syntax.Scope.Monad
scopeWarning'Agda.Syntax.Scope.Monad
ScopingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
scPatsAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
scsub1Agda.Auto.NarrowingSearch
scsub2Agda.Auto.NarrowingSearch
scSubstAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
scTargetAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
scTelAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
sCurMetaAgda.Auto.Convert
searchAboutAgda.Interaction.InteractionTop
secondPartAgda.TypeChecking.Telescope
secTelescopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Section 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SectionApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
SectionSAgda.Syntax.Abstract
SectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sectIsSectionAgda.Syntax.Notation
sectKindAgda.Syntax.Notation
sectLevelAgda.Syntax.Notation
sectNotationAgda.Syntax.Notation
seenUIdsAgda.Auto.Syntax
SelfAgda.Compiler.JS.Syntax
selfAgda.Compiler.JS.Substitution
semiAgda.Syntax.Common.Pretty
SemigroupAgda.Utils.Semigroup, Agda.TypeChecking.Pretty
SemiRingAgda.Utils.SemiRing
Semiring 
1 (Type/Class)Agda.Termination.Semiring
2 (Data Constructor)Agda.Termination.Semiring
sep 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.TypeChecking.Pretty
SeqArg 
1 (Type/Class)Agda.Compiler.Treeless.Subst
2 (Data Constructor)Agda.Compiler.Treeless.Subst
seqcAgda.Auto.NarrowingSearch
seqctxAgda.Auto.CaseSplit
seqPAgda.Utils.Parser.MemoisedCPS
seqPOAgda.Utils.PartialOrd
sEqsAgda.Auto.Convert
sequenceListTAgda.Utils.ListT
SerialisedRange 
1 (Type/Class)Agda.TypeChecking.Serialise.Instances.Common
2 (Data Constructor)Agda.TypeChecking.Serialise.Instances.Common
SerializationAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
SerializeAgda.Utils.ProfileOptions
SeriesAgda.Interaction.JSON
SetAgda.Auto.Syntax
setAgda.Utils.Lens
setAbsoluteIncludePathsAgda.Interaction.Options.Lenses
setAnnotationAgda.Syntax.Common
setArgInfoAgda.Syntax.Common
setArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setAttributeAgda.Syntax.Concrete.Attribute
setAttributesAgda.Syntax.Concrete.Attribute
setBenchmarkingAgda.Utils.Benchmark
SetBindingSiteAgda.Syntax.Scope.Base
setBindingSiteAgda.Syntax.Scope.Base
setBlockingVarOverlapAgda.TypeChecking.Coverage.Match
setBuiltinThingsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCohesionAgda.Syntax.Common
setCohesionModAgda.Syntax.Common
setCommandLineOptions 
1 (Function)Agda.Interaction.Options.Lenses
2 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCommandLineOptions'Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCommandLineOptsAgda.Interaction.InteractionTop
setCompiledArgUseAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCompiledClausesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setConNameAgda.Syntax.Internal
setContextAgda.Syntax.Parser.Monad
setContextPrecedenceAgda.Syntax.Scope.Monad
setCurrentModuleAgda.Syntax.Scope.Monad
setCurrentRangeAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setDebuggingAgda.TypeChecking.SizedTypes.Utils
setDecodedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setDefaultAgda.Utils.WithDefault
setErasedConArgsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setFoldlAgda.TypeChecking.SizedTypes.WarshallSolver
setFreeVariablesAgda.Syntax.Common
setFreeVariablesArgInfoAgda.Syntax.Common
setFunctionFlagAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setHardCompileTimeModeIfErasedAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setHardCompileTimeModeIfErased'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setHidingAgda.Syntax.Common
setHidingArgInfoAgda.Syntax.Common
setImportedNameAgda.Syntax.Common
setIncludeDirsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setIncludePathsAgda.Interaction.Options.Lenses
setInputAgda.Syntax.Parser.LookAhead
setInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setInteractionOutputCallbackAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setInterfaceAgda.Compiler.Common
setIntervalFileAgda.Syntax.Position
setLastPosAgda.Syntax.Parser.Monad
setLexInputAgda.Syntax.Parser.Alex
setLibraryIncludesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setLibraryPathsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setLocalVarsAgda.Syntax.Scope.Monad
setLockAgda.Syntax.Common
setMatchableSymbolsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaGeneralizableArgInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaNameSuggestionAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaOccursCheckAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setModalityAgda.Syntax.Common
setModalityArgInfoAgda.Syntax.Common
setModeUnlessInHardCompileTimeModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setModuleCheckpointAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMutualAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMutualBlockInfoAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setNamedArgAgda.Syntax.Common
setNamedScopeAgda.Syntax.Scope.Monad
setNameOfAgda.Syntax.Common
setNameSpaceAgda.Syntax.Scope.Base
setNameSuffixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setNotInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setOptionsFromPragmaAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setOriginAgda.Syntax.Common
setOriginArgInfoAgda.Syntax.Common
setParsePosAgda.Syntax.Parser.Monad
setPatternSynsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setPersistentVerbosityAgda.Interaction.Options.Lenses
setPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setPragmaOptions 
1 (Function)Agda.Interaction.Options.Lenses
2 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setPrevTokenAgda.Syntax.Parser.Monad
setPristineAttributeAgda.Syntax.Concrete.Attribute
setPristineAttributesAgda.Syntax.Concrete.Attribute
setPristineCohesionAgda.Syntax.Concrete.Attribute
setPristineLockAgda.Syntax.Concrete.Attribute
setPristineQuantityAgda.Syntax.Concrete.Attribute
setPristineRelevanceAgda.Syntax.Concrete.Attribute
setPtrAgda.Utils.Pointer
setQuantityAgda.Syntax.Common
setQuantityModAgda.Syntax.Common
SetRange 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setRangeAgda.Syntax.Position
setRelevanceAgda.Syntax.Common
setRelevanceModAgda.Syntax.Common
setRunTimeModeUnlessInHardCompileTimeModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SetSAgda.Syntax.Reflected
setSafeModeAgda.Interaction.Options.Lenses
setScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setScopeAccessAgda.Syntax.Scope.Base
setScopeLocalsAgda.Syntax.Scope.Base
setSignatureAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setSplitTreeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTCLensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTCLens'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTerminatesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SetToInftyAgda.TypeChecking.SizedTypes.WarshallSolver
setToInftyAgda.TypeChecking.SizedTypes.WarshallSolver
setTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTreelessAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setUsabilityAgda.Termination.Order
setValueMetaNameAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setVarsToBindAgda.Syntax.Scope.Base
setVerbosityAgda.Interaction.Options.Lenses
setVisitedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
severalAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
SeveralConstructorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SFalseAgda.Utils.TypeLits
sgListTAgda.Utils.ListT
sgMListTAgda.Utils.ListT
SgTelAgda.Syntax.Internal
sgTelAgda.Syntax.Internal
ShadowedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShadowingInTelescope 
1 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
ShadowingInTelescope_Agda.Interaction.Options.Warnings
shadowLocalAgda.Syntax.Scope.Base
SharingAgda.Utils.ProfileOptions
sharingAgda.Utils.Update
shiftAgda.Compiler.JS.Substitution
shifterAgda.Compiler.JS.Substitution
shiftFromAgda.Compiler.JS.Substitution
ShouldAcceptAtLeastTwoArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeApplicationOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeAppliedToTheDatatypeParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeASortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBePathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBePathAgda.TypeChecking.Telescope
ShouldBePiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBePiAgda.TypeChecking.Telescope
shouldBePiOrPathAgda.TypeChecking.Telescope
shouldBeProjectibleAgda.TypeChecking.Records
ShouldBeRecordPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBeSortAgda.TypeChecking.Sort
ShouldEndInApplicationOfTheDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldPostponeInstanceSearchAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.TypeChecking.InstanceArguments, Agda.Compiler.Backend
shouldReduceDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showAAgda.Syntax.Abstract.Pretty
showATopAgda.Syntax.Abstract.Pretty
showChar'Agda.Syntax.Literal
showComputedAgda.Interaction.BasicOps
showGeneralizedArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showGoalsAgda.Interaction.BasicOps, Agda.Interaction.EmacsTop
ShowHeadAgda.TypeChecking.Rules.Decl
showHeadAgda.TypeChecking.Rules.Decl
showIdentitySubstitutionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShowImplicitArgsAgda.Interaction.Base
showImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showInfoErrorAgda.Interaction.EmacsTop
ShowIrrelevantArgsAgda.Interaction.Base
showIrrelevantArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showModuleContentsAgda.Interaction.InteractionTop
showQNameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
showTextAgda.Syntax.Literal
showThousandSepAgda.Utils.String
showUnivAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
SideconditionAgda.Auto.NarrowingSearch
SigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigAbstractAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigCubicalNotErasureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigDefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigErrorAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigErrorAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigmaConAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
sigmaFstAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
SigmaKit 
1 (Type/Class)Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
2 (Data Constructor)Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
sigmaNameAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
sigmaSndAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
SignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigRewriteRulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigSectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigUnknownAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
simpleBinaryOperatorAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
simpleHoleAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
simpleNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
SimplificationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SimplifiedAgda.Interaction.Base
SimplifyAgda.TypeChecking.Reduce
simplifyAgda.TypeChecking.Reduce
simplify1Agda.TypeChecking.SizedTypes.Syntax
simplifyBlocked'Agda.TypeChecking.Reduce
simplifyLevelConstraintAgda.TypeChecking.LevelConstraints
simplifyTTermAgda.Compiler.Treeless.Simplify
simplifyWithHypothesesAgda.TypeChecking.SizedTypes.WarshallSolver
SingleClosedAgda.TypeChecking.Level
singleConstructorTypeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SingleLevelAgda.TypeChecking.Level
SingleLevel'Agda.TypeChecking.Level
singleLevelViewAgda.TypeChecking.Level
SinglePlusAgda.TypeChecking.Level
SingletonAgda.Utils.Singleton
singleton 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.VarSet
3 (Function)Agda.Utils.BoolSet
4 (Function)Agda.Utils.Bag
5 (Function)Agda.Utils.IntSet.Infinite
6 (Function)Agda.Utils.SmallSet
7 (Function)Agda.Utils.Singleton
8 (Function)Agda.Utils.Trie
9 (Function)Agda.Utils.BiMap
10 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
11 (Function)Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
SingletonRecordsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
singletonSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SingleVarAgda.TypeChecking.Free.Lazy
singPluralAgda.Syntax.Common.Pretty
Size 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
size 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.Size
4 (Function)Agda.Termination.SparseMatrix
sizeAndBoundVarsAgda.Auto.CaseSplit
sizeBuiltinsAgda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeConstAgda.Utils.Warshall
SizeConstraintAgda.TypeChecking.SizedTypes.Solve
sizeConstraintAgda.TypeChecking.SizedTypes.Solve
sizeContextAgda.TypeChecking.SizedTypes.Solve
SizedAgda.Utils.Size
sizedTextAgda.Syntax.Common.Pretty
SizedThing 
1 (Type/Class)Agda.Utils.Size
2 (Data Constructor)Agda.Utils.Size
sizedThingAgda.Utils.Size
sizedTypesOptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeExpr 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
sizeExprAgda.TypeChecking.SizedTypes.Solve
SizeExpr'Agda.TypeChecking.SizedTypes.Syntax
sizeHypIdsAgda.TypeChecking.SizedTypes.Solve
sizeHypothesesAgda.TypeChecking.SizedTypes.Solve
SizeInfAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeLtSatAgda.Interaction.Base
sizeMaxAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeMaxViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeMaxViewAgda.TypeChecking.SizedTypes
SizeMaxView'Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeMeta 
1 (Data Constructor)Agda.TypeChecking.SizedTypes
2 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
3 (Data Constructor)Agda.TypeChecking.SizedTypes.Solve
sizeMetaArgsAgda.TypeChecking.SizedTypes.Solve
sizeMetaIdAgda.TypeChecking.SizedTypes.Solve
SizeOfSort 
1 (Type/Class)Agda.TypeChecking.Substitute
2 (Data Constructor)Agda.TypeChecking.Substitute
sizeOfSortAgda.TypeChecking.Substitute
sizeRigidAgda.Utils.Warshall
sizeSortAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeSucNameAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeSuc_Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeThingAgda.Utils.Size
sizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeType_Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeUnivAgda.Syntax.Internal
sizeUnivAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeVarAgda.Utils.Warshall
SizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeViewComparableAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewComparableAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewComparableWithMaxAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewOffsetAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewPredAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewSuc_Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Skip 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Compiler.Backend
skipAgda.Syntax.Parser.LexActions
skipBlockAgda.Syntax.Parser.Comments
skipIrrelevantAtAgda.TypeChecking.Rules.LHS.Unify.Types
SkipIrrelevantEquationAgda.TypeChecking.Rules.LHS.Unify.Types
SleepingConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
slowNormaliseArgsAgda.TypeChecking.Reduce
slowReduceTermAgda.TypeChecking.Reduce
sMainMetaAgda.Auto.Convert
smallestAgda.TypeChecking.SizedTypes.WarshallSolver
SmallSetAgda.Utils.SmallSet
SmallSetElementAgda.Utils.SmallSet
SmallSortAgda.TypeChecking.Substitute
smashTelAgda.Syntax.Concrete.Pretty
sMetasAgda.Auto.Convert
snd3Agda.Utils.Tuple
snoc 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
SolAgda.Auto.CaseSplit
Solution 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
4 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify.Types
solutionAtAgda.TypeChecking.Rules.LHS.Unify.Types
SolutionsAgda.Auto.Auto
solutionSideAgda.TypeChecking.Rules.LHS.Unify.Types
solutionTermAgda.TypeChecking.Rules.LHS.Unify.Types
solutionTypeAgda.TypeChecking.Rules.LHS.Unify.Types
solutionVarAgda.TypeChecking.Rules.LHS.Unify.Types
solveAgda.Utils.Warshall
solveAwakeConstraintsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveAwakeConstraints'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveAwakeInstanceConstraintsAgda.TypeChecking.InstanceArguments
solveClusterAgda.TypeChecking.SizedTypes.Solve
solveConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveConstraintTCMAgda.TypeChecking.Constraints
solveConstraint_Agda.TypeChecking.Constraints
SolvedButOpenHolesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solvedMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveEqAgda.TypeChecking.Rules.LHS.Unify.Types
solveGraphAgda.TypeChecking.SizedTypes.WarshallSolver
solveGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
solveInstantiatedGoalsAgda.Interaction.InteractionTop
solveSizeConstraintsAgda.TypeChecking.SizedTypes.Solve
solveSizeConstraints_Agda.TypeChecking.SizedTypes.Solve
solveSomeAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveSomeAwakeConstraintsTCMAgda.TypeChecking.Constraints
solveVarAgda.TypeChecking.Rules.LHS.Unify.Types
solvingProblemAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solvingProblemsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Some 
1 (Type/Class)Agda.Utils.IndexedList
2 (Data Constructor)Agda.Utils.IndexedList
some1Agda.Utils.List1
SomeBuiltinAgda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
someBuiltinAgda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SomeGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SomeKindsOfNamesAgda.Syntax.Scope.Base
someKindsOfNamesAgda.Syntax.Scope.Base
SomeWhereAgda.Syntax.Concrete
Sort 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.Auto.Syntax
3 (Type/Class)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Internal
5 (Type/Class)Agda.Syntax.Reflected
6 (Data Constructor)Agda.Syntax.Reflected
7 (Data Constructor)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
sort 
1 (Function)Agda.Utils.List1
2 (Function)Agda.TypeChecking.Substitute
Sort'Agda.Syntax.Internal
sortByAgda.Utils.List1
SortCannotDependOnItsIndexAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortDefsAgda.Compiler.Common
SortDoesNotAdmitDataDefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortedAgda.Utils.List
sortFitsInAgda.TypeChecking.Sort
SortHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortInteractionPointsAgda.Interaction.InteractionTop
SortIntervalUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortKit 
1 (Type/Class)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortKitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortLevelUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortOfAgda.TypeChecking.Sort
SortOfSplitVarErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortOfTypeAgda.TypeChecking.Sort
SortOmegaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortPropAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortPropOmegaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortRulesOfSymbolAgda.TypeChecking.Rewriting.Confluence
SortSetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortSetOmegaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortStrictSetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortStrictSetOmegaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortWithAgda.Utils.List1
Source 
1 (Type/Class)Agda.Interaction.Imports
2 (Data Constructor)Agda.Interaction.Imports
source 
1 (Function)Agda.Utils.BiMap
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
SourceFile 
1 (Type/Class)Agda.Interaction.FindFile
2 (Data Constructor)Agda.Interaction.FindFile
sourceNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
SpaceAgda.Compiler.JS.Pretty
space 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.Compiler.JS.Pretty
Span 
1 (Type/Class)Agda.Syntax.Common.Pretty
2 (Data Constructor)Agda.Syntax.Common.Pretty
spanAgda.Utils.List1
spanAllowedBeforeModuleAgda.Syntax.Concrete
spanAnnotationAgda.Syntax.Common.Pretty
spanEndAgda.Utils.List
spanJustAgda.Utils.List
spanLengthAgda.Syntax.Common.Pretty
spanMaybeAgda.Utils.Maybe
spanStartAgda.Syntax.Common.Pretty
SpecialCharacters 
1 (Type/Class)Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
2 (Data Constructor)Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
specialCharactersForGlyphsAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
SpecifiedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpeculateAbortAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpeculateCommitAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
speculateMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpeculateResultAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
speculateTCStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
speculateTCState_Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpineClauseAgda.Syntax.Abstract
SpineLHS 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
spineToLhsAgda.Syntax.Abstract.Pattern
spineToLhsCoreAgda.Syntax.Abstract.Pattern
spLhsDefNameAgda.Syntax.Abstract
spLhsInfoAgda.Syntax.Abstract
spLhsPatsAgda.Syntax.Abstract
splitApplyElimsAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
splitArgAgda.TypeChecking.Coverage.SplitTree
SplitAtAgda.TypeChecking.Coverage.SplitTree
splitAt 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.RangeMap
splitBindingsAgda.TypeChecking.Coverage.SplitTree
splitCAgda.TypeChecking.CompiledClause.Compile
SplitCatchallAgda.TypeChecking.Coverage.SplitTree
SplitClauseAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
splitClausesAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
splitClauseWithAbsurdAgda.TypeChecking.Coverage
splitCommasAgda.Interaction.Library.Parse
SplitConAgda.TypeChecking.Coverage.SplitTree
splitEllipsisAgda.Syntax.Concrete.Pattern
SplitError 
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
splitExactlyAtAgda.Utils.List
splitExcludedLitsAgda.TypeChecking.Coverage.Match
SplitInPropAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
splitLastAgda.TypeChecking.Coverage
splitLazyAgda.TypeChecking.Coverage.SplitTree
SplitLitAgda.TypeChecking.Coverage.SplitTree
splitOffTrailingWithPatternsAgda.Syntax.Abstract.Pattern
splitOnAgda.TypeChecking.CompiledClause.Compile
SplitOnAbstractAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
splitOnDotsAgda.Syntax.Parser.Parser
SplitOnFlatAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
SplitOnIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnNonEtaRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnNonVariableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnPartialAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnStrictAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
SplitOnUncheckedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnUnusableCohesionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitPatternAgda.TypeChecking.Coverage.Match
SplitPatVar 
1 (Type/Class)Agda.TypeChecking.Coverage.Match
2 (Data Constructor)Agda.TypeChecking.Coverage.Match
splitPatVarIndexAgda.TypeChecking.Coverage.Match
splitPatVarNameAgda.TypeChecking.Coverage.Match
splitPermAgda.TypeChecking.Telescope
splitResultAgda.TypeChecking.Coverage
splitSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
splittableCohesionAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitTagAgda.TypeChecking.Coverage.SplitTree
SplitTel 
1 (Type/Class)Agda.TypeChecking.Telescope
2 (Data Constructor)Agda.TypeChecking.Telescope
splitTelescopeAgda.TypeChecking.Telescope
splitTelescopeAtAgda.TypeChecking.Telescope
splitTelescopeExactAgda.TypeChecking.Telescope
splitTelForWithAgda.TypeChecking.With
SplittingDoneAgda.TypeChecking.Coverage.SplitTree
SplitTreeAgda.TypeChecking.Coverage.SplitTree
SplitTree'Agda.TypeChecking.Coverage.SplitTree
SplitTreeLabel 
1 (Type/Class)Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor)Agda.TypeChecking.Coverage.SplitTree
SplitTreesAgda.TypeChecking.Coverage.SplitTree
splitTreesAgda.TypeChecking.Coverage.SplitTree
SplitTrees'Agda.TypeChecking.Coverage.SplitTree
squareAgda.Termination.SparseMatrix
SquashAgda.Syntax.Common
srcAgda.TypeChecking.SizedTypes.WarshallSolver
srcAttributesAgda.Interaction.Imports
SrcFileAgda.Syntax.Position
srcFileAgda.Syntax.Position
srcFilePathAgda.Interaction.FindFile
srcFileTypeAgda.Interaction.Imports
SrcFunAgda.Utils.CallStack
SrcLoc 
1 (Data Constructor)Agda.Utils.CallStack
2 (Type/Class)Agda.Utils.CallStack
SrcLocColAgda.Utils.CallStack
srcLocEndColAgda.Utils.CallStack
srcLocEndLineAgda.Utils.CallStack
SrcLocFileAgda.Utils.CallStack
srcLocFileAgda.Utils.CallStack
SrcLocLineAgda.Utils.CallStack
SrcLocModuleAgda.Utils.CallStack
srcLocModuleAgda.Utils.CallStack
SrcLocPackageAgda.Utils.CallStack
srcLocPackageAgda.Utils.CallStack
srcLocStartColAgda.Utils.CallStack
srcLocStartLineAgda.Utils.CallStack
srcModuleAgda.Interaction.Imports
srcModuleNameAgda.Interaction.Imports
srcNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
srcOriginAgda.Interaction.Imports
srcProjectLibsAgda.Interaction.Imports
srcTextAgda.Interaction.Imports
SResAgda.Auto.NarrowingSearch
SSetAgda.Syntax.Internal
sShowImplicitArgumentsAgda.Interaction.Response
sShowIrrelevantArgumentsAgda.Interaction.Response
sSizeUnivAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
ssortAgda.TypeChecking.Substitute
SSSMismatchAgda.Utils.List
SSSResultAgda.Utils.List
SSSStripAgda.Utils.List
St 
1 (Type/Class)Agda.TypeChecking.Serialise.Base
2 (Data Constructor)Agda.TypeChecking.Serialise.Base
stAccumStatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StackAgda.TypeChecking.CompiledClause.Match
stAgdaLibFilesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
standardOptionsAgda.Interaction.Options
standardOptions_Agda.Interaction.Options
stAreWeCachingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
starPAgda.Utils.Parser.MemoisedCPS
StarSemiRingAgda.Utils.SemiRing
startPosAgda.Syntax.Position
startPos'Agda.Syntax.Position
stateTCLensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stateTCLensMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StaticPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
StatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
statsAgda.TypeChecking.Serialise.Base
Status 
1 (Type/Class)Agda.Interaction.Response
2 (Data Constructor)Agda.Interaction.Response
statusAgda.Interaction.InteractionTop
stAwakeConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stBackendsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stBenchmarkAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stBuiltinThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stConsideringInstanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stCopiedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StdErrAgda.TypeChecking.Unquote
StdInAgda.TypeChecking.Unquote
stDirtyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StdOutAgda.TypeChecking.Unquote
stealConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stealConstraintsTCMAgda.TypeChecking.Constraints
sTextCAgda.TypeChecking.Serialise.Base
sTextDAgda.TypeChecking.Serialise.Base
sTextEAgda.TypeChecking.Serialise.Base
stForeignCodeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshCheckpointIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshIntAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshInteractionIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshMetaIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshMutualIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshNameIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshOpaqueIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshProblemIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedDisplayFormsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedInstanceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedPartialDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedUserWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportsDisplayFormsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInstanceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInstantiateBlockingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInteractionOutputCallbackAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLoadedFileCacheAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLocalBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLocalPartialDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLocalUserWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stModuleToSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StmtAgda.Utils.Haskell.Syntax
stMutualBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stNameCopiesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOccursCheckDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOpaqueBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOpaqueIdsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOpenMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeCachedAgdaLibFileAgda.Interaction.Library.Base
storeCachedProjectConfigAgda.Interaction.Library.Base
storeDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeDisambiguatedConstructorAgda.Interaction.Highlighting.Generate
storeDisambiguatedProjectionAgda.Interaction.Highlighting.Generate
stPatternSynImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPatternSynsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistBackendsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentTopLevelModuleNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistLoadedFileCacheAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostAreWeCachingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostAwakeConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostConsideringInstanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostDirtyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostDisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshCheckpointIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshIntAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshMetaIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshMutualIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshNameIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshOpaqueIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshProblemIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostImportsDisplayFormsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostInstanceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostInstantiateBlockingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostInteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostLocalBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostLocalPartialDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostMutualBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOccursCheckDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOpaqueBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOpaqueIdsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOpenMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostponeInstanceSearchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostPostponeInstanceSearchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostScopeStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostShadowingNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSleepingConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSolvedMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostStatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSyntaxInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostTCWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostUsedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreAgdaLibFilesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreCopiedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreForeignCodeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreFreshInteractionIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedDisplayFormsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedInstanceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedPartialDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedUserWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreLocalUserWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreModuleToSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreNameCopiesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrePatternSynImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrePatternSynsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrePragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreProjectConfigsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreScopeStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreTokensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreVisitedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreWarningOnImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stProjectConfigsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StrengthenAgda.Syntax.Internal, Agda.TypeChecking.Substitute
strengthenAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
strengthenSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
strengthenS'Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Strict 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Type/Class)Agda.Utils.Maybe.Strict
strictCurryAgda.Utils.TypeLevel
StrictCurryingAgda.Utils.TypeLevel
strictCurrysAgda.Utils.TypeLevel
StrictnessAgda.Utils.Haskell.Syntax
StrictPairAgda.Utils.TypeLevel
StrictPosAgda.TypeChecking.Positivity.Occurrence
StrictProductsAgda.Utils.TypeLevel
StrictSplitAgda.TypeChecking.Coverage.SplitTree
strictUncurryAgda.Utils.TypeLevel
strictUncurrysAgda.Utils.TypeLevel
String 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Compiler.JS.Syntax
4 (Data Constructor)Agda.Interaction.JSON
String1Agda.Utils.List1
string2HelpTopicAgda.Interaction.Options.Help
string2WarningNameAgda.Interaction.Options.Warnings
stringCAgda.TypeChecking.Serialise.Base
stringDAgda.TypeChecking.Serialise.Base
stringEAgda.TypeChecking.Serialise.Base
stringNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
stringPartsAgda.Syntax.Notation
stringTCErrAgda.TypeChecking.Errors
stringToArgNameAgda.Syntax.Common
stringToAttributeAgda.Syntax.Concrete.Attribute
stringToRawNameAgda.Syntax.Common
stripArgLeftAgda.TypeChecking.Rules.LHS.Unify.Types
stripArgRightAgda.TypeChecking.Rules.LHS.Unify.Types
stripAtAgda.TypeChecking.Rules.LHS.Unify.Types
stripConstraintPidsAgda.Interaction.BasicOps
stripDontCareAgda.Syntax.Internal
stripNoNamesAgda.Syntax.Scope.Monad
stripPrefixByAgda.Utils.List
stripReversedSuffixAgda.Utils.List
stripRTSAgda.Interaction.Options
StripSizeSucAgda.TypeChecking.Rules.LHS.Unify.Types
stripSuffixAgda.Utils.List
stripUnusedArgumentsAgda.Compiler.Treeless.Unused
stripWithClausePatternsAgda.TypeChecking.With
stronglyAgda.TypeChecking.MetaVars.Occurs
StronglyRigidAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
stronglyRigidVarsAgda.TypeChecking.Free
StrPartAgda.TypeChecking.Unquote
StrSufStAgda.Utils.List
STrueAgda.Utils.TypeLits
stScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stShadowingNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSleepingConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSolvedMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stStatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSyntaxInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTCWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTokensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTopLevelModuleNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StuckOnAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stuckOnAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stUsedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stVisitedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stWarningOnImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Style 
1 (Type/Class)Agda.Syntax.Common.Pretty
2 (Data Constructor)Agda.Syntax.Common.Pretty
styleAgda.Syntax.Common.Pretty
Sub 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
subAgda.Auto.Syntax
SubConstraints 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
subiAgda.Auto.Syntax
subLevelAgda.TypeChecking.Level
SubscriptAgda.Utils.Suffix
SubstAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subst 
1 (Function)Agda.Compiler.JS.Substitution
2 (Function)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
3 (Function)Agda.TypeChecking.SizedTypes.Syntax
subst'Agda.Compiler.JS.Substitution
SubstArgAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute, Agda.TypeChecking.Substitute
substBodyAgda.TypeChecking.CompiledClause.Compile
SubstCandAgda.TypeChecking.MetaVars
SubstExprAgda.Syntax.Abstract
substExprAgda.Syntax.Abstract
SubstituteAgda.TypeChecking.SizedTypes.Syntax
substituterAgda.Compiler.JS.Substitution
Substitution 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Syntax.Internal, Agda.TypeChecking.Substitute
Substitution'Agda.Syntax.Internal, Agda.TypeChecking.Substitute
substPatternAgda.Syntax.Abstract.Pattern
substPattern'Agda.Syntax.Abstract.Pattern
substUnderAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SubstWithAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subsvarsAgda.Auto.SearchControl
subtractAgda.Utils.VarSet
subtypingForSizeLtAgda.TypeChecking.MetaVars
subVarAgda.TypeChecking.Free.Lazy
SucAgda.Utils.IndexedList
SuccAgda.Utils.Size
sucNameAgda.TypeChecking.Level
Suffix 
1 (Type/Class)Agda.Utils.Suffix
2 (Type/Class)Agda.Utils.List
3 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
suffixesSatisfyingAgda.Utils.List
suffixNameSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
suffixToLevelAgda.TypeChecking.Rules.Application
suffixViewAgda.Utils.Suffix
SuggestAgda.Syntax.Internal
Suggestion 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
suggestNameAgda.Syntax.Internal
suggestsAgda.Syntax.Internal
SumEncodingAgda.Interaction.JSON
sumEncodingAgda.Interaction.JSON
supremumAgda.Termination.Order
supSizeAgda.Termination.SparseMatrix
swapAgda.Utils.Tuple
swap01Agda.TypeChecking.Abstract
swapEitherAgda.Utils.Either
switchBenchmarkingAgda.Utils.Benchmark
SymArrowAgda.Syntax.Parser.Tokens
SymAsAgda.Syntax.Parser.Tokens
SymBarAgda.Syntax.Parser.Tokens
Symbol 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
3 (Type/Class)Agda.Syntax.Parser.Tokens
symbolAgda.Syntax.Parser.LexActions
SymCloseBraceAgda.Syntax.Parser.Tokens
SymCloseIdiomBracketAgda.Syntax.Parser.Tokens
SymCloseParenAgda.Syntax.Parser.Tokens
SymClosePragmaAgda.Syntax.Parser.Tokens
SymCloseVirtualBraceAgda.Syntax.Parser.Tokens
SymColonAgda.Syntax.Parser.Tokens
SymDotAgda.Syntax.Parser.Tokens
SymDotDotAgda.Syntax.Parser.Tokens
SymDoubleCloseBraceAgda.Syntax.Parser.Tokens
SymDoubleOpenBraceAgda.Syntax.Parser.Tokens
SymEllipsisAgda.Syntax.Parser.Tokens
SymEmptyIdiomBracketAgda.Syntax.Parser.Tokens
SymEndCommentAgda.Syntax.Parser.Tokens
SymEqualAgda.Syntax.Parser.Tokens
SymLambdaAgda.Syntax.Parser.Tokens
SymOpenBraceAgda.Syntax.Parser.Tokens
SymOpenIdiomBracketAgda.Syntax.Parser.Tokens
SymOpenParenAgda.Syntax.Parser.Tokens
SymOpenPragmaAgda.Syntax.Parser.Tokens
SymOpenVirtualBraceAgda.Syntax.Parser.Tokens
SymQuestionMarkAgda.Syntax.Parser.Tokens
SymSemiAgda.Syntax.Parser.Tokens
SymUnderscoreAgda.Syntax.Parser.Tokens
SymVirtualSemiAgda.Syntax.Parser.Tokens
syncAgda.Syntax.Parser.LookAhead
SynEqAgda.TypeChecking.SyntacticEquality
syntacticEqualityFuelRemainsAgda.TypeChecking.SyntacticEquality
SyntaxAgda.Syntax.Concrete
SyntaxBindingLambdaAgda.Syntax.Concrete
syntaxOfAgda.Syntax.Notation
System 
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
systemClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
systemTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
szSortSizeAgda.TypeChecking.Substitute
szSortUnivAgda.TypeChecking.Substitute