Agda-2.6.2.1.20220327: 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
safeFlagAgda.Interaction.Options
SafeFlagEtaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagEta_Agda.Interaction.Options.Warnings
SafeFlagInjectiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagInjective_Agda.Interaction.Options.Warnings
SafeFlagNoCoverageCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNoCoverageCheck_Agda.Interaction.Options.Warnings
SafeFlagNonTerminatingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNonTerminating_Agda.Interaction.Options.Warnings
SafeFlagNoPositivityCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNoPositivityCheck_Agda.Interaction.Options.Warnings
SafeFlagNoUniverseCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNoUniverseCheck_Agda.Interaction.Options.Warnings
SafeFlagPolarityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagPolarity_Agda.Interaction.Options.Warnings
SafeFlagPostulateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagPostulate_Agda.Interaction.Options.Warnings
SafeFlagPragmaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagPragma_Agda.Interaction.Options.Warnings
SafeFlagTerminatingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagTerminating_Agda.Interaction.Options.Warnings
SafeFlagWithoutKFlagPrimEraseEqualityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagWithoutKFlagPrimEraseEquality_Agda.Interaction.Options.Warnings
SafeModeAgda.Interaction.Options.Lenses
safePermuteAgda.Utils.Permutation
sameCohesionAgda.Syntax.Common
sameDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
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
sccomcountAgda.Auto.NarrowingSearch
sccsAgda.Utils.Graph.AdjacencyMap.Unidirectional
sccs'Agda.Utils.Graph.AdjacencyMap.Unidirectional
scflipAgda.Auto.NarrowingSearch
sCheckedAgda.Interaction.Response
SClauseAgda.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.Compiler.Backend, Agda.TypeChecking.Monad
ScopeCheckExprAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
scopeCheckImportAgda.Interaction.Imports
scopeCheckingSufficesAgda.Compiler.Backend
ScopeCheckLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ScopeCopyInfo 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
scopeCurrentAgda.Syntax.Scope.Base
scopeDatatypeModuleAgda.Syntax.Scope.Base
ScopedDeclAgda.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
scsub1Agda.Auto.NarrowingSearch
scsub2Agda.Auto.NarrowingSearch
scSubstAgda.TypeChecking.Coverage
scTargetAgda.TypeChecking.Coverage
scTelAgda.TypeChecking.Coverage
sCurMetaAgda.Auto.Convert
searchAboutAgda.Interaction.InteractionTop
secondPartAgda.TypeChecking.Telescope
secTelescopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Section 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SectionApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
SectionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sectIsSectionAgda.Syntax.Notation
sectKindAgda.Syntax.Notation
sectLevelAgda.Syntax.Notation
sectNotationAgda.Syntax.Notation
seenUIdsAgda.Auto.Syntax
SelfAgda.Compiler.JS.Syntax
selfAgda.Compiler.JS.Substitution
semiAgda.Utils.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.Utils.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
SeriesAgda.Interaction.JSON
SetAgda.Auto.Syntax
setAgda.Utils.Lens
setAbsoluteIncludePathsAgda.Interaction.Options.Lenses
setAnnotationAgda.Syntax.Common
setArgInfoAgda.Syntax.Common
setArgOccurrencesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setAttributeAgda.Syntax.Concrete.Attribute
setAttributesAgda.Syntax.Concrete.Attribute
setBenchmarkingAgda.Utils.Benchmark
SetBindingSiteAgda.Syntax.Scope.Base
setBindingSiteAgda.Syntax.Scope.Base
setBlockingVarOverlapAgda.TypeChecking.Coverage.Match
setBuiltinThingsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
setCohesionAgda.Syntax.Common
setCohesionModAgda.Syntax.Common
setCommandLineOptions 
1 (Function)Agda.Interaction.Options.Lenses
2 (Function)Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setCommandLineOptions'Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setCommandLineOptsAgda.Interaction.InteractionTop
setCompiledArgUseAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setCompiledClausesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setConNameAgda.Syntax.Internal
setContextAgda.Syntax.Parser.Monad
setContextPrecedenceAgda.Syntax.Scope.Monad
setCurrentModuleAgda.Syntax.Scope.Monad
setCurrentRangeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
setDebuggingAgda.TypeChecking.SizedTypes.Utils
setDecodedModulesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
setDefaultAgda.Utils.WithDefault
setErasedConArgsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setEtaEqualityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setFoldlAgda.TypeChecking.SizedTypes.WarshallSolver
setFreeVariablesAgda.Syntax.Common
setFreeVariablesArgInfoAgda.Syntax.Common
setFunctionFlagAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setHidingAgda.Syntax.Common
setHidingArgInfoAgda.Syntax.Common
setImportedNameAgda.Syntax.Common
setIncludeDirsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setIncludePathsAgda.Interaction.Options.Lenses
setInputAgda.Syntax.Parser.LookAhead
setInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setInteractionOutputCallbackAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setInterfaceAgda.Compiler.Common
setIntervalFileAgda.Syntax.Position
setLastPosAgda.Syntax.Parser.Monad
setLexInputAgda.Syntax.Parser.Alex
setLibraryIncludesAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setLibraryPathsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setLocalVarsAgda.Syntax.Scope.Monad
setLockAgda.Syntax.Common
setMatchableSymbolsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setMetaGeneralizableArgInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setMetaNameSuggestionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setMetaOccursCheckAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setModalityAgda.Syntax.Common
setModalityArgInfoAgda.Syntax.Common
setModuleCheckpointAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setMutualAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setMutualBlockAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
setMutualBlockInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
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.Compiler.Backend, Agda.TypeChecking.Monad
setOriginAgda.Syntax.Common
setOriginArgInfoAgda.Syntax.Common
setParsePosAgda.Syntax.Parser.Monad
setPatternSynsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setPersistentVerbosityAgda.Interaction.Options.Lenses
setPolarityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setPragmaOptions 
1 (Function)Agda.Interaction.Options.Lenses
2 (Function)Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
setRangeAgda.Syntax.Position
setRelevanceAgda.Syntax.Common
setRelevanceModAgda.Syntax.Common
SetSAgda.Syntax.Reflected
setSafeModeAgda.Interaction.Options.Lenses
setScopeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setScopeAccessAgda.Syntax.Scope.Base
setScopeLocalsAgda.Syntax.Scope.Base
setSignatureAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setSplitTreeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setTCLensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setTerminatesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
SetToInftyAgda.TypeChecking.SizedTypes.WarshallSolver
setToInftyAgda.TypeChecking.SizedTypes.WarshallSolver
setTopLevelModuleAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setTreelessAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setUsabilityAgda.Termination.Order
setValueMetaNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setVarsToBindAgda.Syntax.Scope.Base
setVerbosityAgda.Interaction.Options.Lenses
setVisitedModulesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
severalAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
SFalseAgda.Utils.TypeLits
sgListTAgda.Utils.ListT
sgMListTAgda.Utils.ListT
SgTelAgda.Syntax.Internal
sgTelAgda.Syntax.Internal
ShadowedModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShadowingInTelescope 
1 (Data Constructor)Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
ShadowingInTelescope_Agda.Interaction.Options.Warnings
shadowLocalAgda.Syntax.Scope.Base
sharingAgda.Utils.Update
shiftAgda.Compiler.JS.Substitution
shifterAgda.Compiler.JS.Substitution
shiftFromAgda.Compiler.JS.Substitution
ShouldBeApplicationOfAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeAppliedToTheDatatypeParametersAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeASortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeEmptyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBePathAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBePiAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeRecordPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeRecordTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
shouldBeSortAgda.TypeChecking.Sort, Agda.TypeChecking.CheckInternal
ShouldEndInApplicationOfTheDatatypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
shouldPostponeInstanceSearchAgda.TypeChecking.InstanceArguments
shouldReduceDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
shouldTryFastReduceAgda.TypeChecking.Reduce
showAAgda.Syntax.Abstract.Pretty
showATopAgda.Syntax.Abstract.Pretty
showChar'Agda.Syntax.Literal
showComputedAgda.Interaction.BasicOps
showGoalsAgda.Interaction.BasicOps, Agda.Interaction.EmacsTop
ShowHeadAgda.TypeChecking.Rules.Decl
showHeadAgda.TypeChecking.Rules.Decl
showIdentitySubstitutionsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShowImplicitArgsAgda.Interaction.Base
showImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
showInfoErrorAgda.Interaction.EmacsTop
ShowIrrelevantArgsAgda.Interaction.Base
showIrrelevantArgumentsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
SideconditionAgda.Auto.NarrowingSearch
SigAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SigAbstractAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sigDefinitionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SigErrorAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sigErrorAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sigmaConAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
sigmaFstAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
SigmaKit 
1 (Type/Class)Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
2 (Data Constructor)Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
sigmaNameAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
sigmaSndAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
SignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sigRewriteRulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sigSectionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SigUnknownAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad
SimplifiedAgda.Interaction.Base
SimplifyAgda.TypeChecking.Reduce
simplifyAgda.TypeChecking.Reduce
simplify'Agda.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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Bag
4 (Function)Agda.Utils.IntSet.Infinite
5 (Function)Agda.Utils.Singleton
6 (Function)Agda.Utils.SmallSet
7 (Function)Agda.Utils.Trie
8 (Function)Agda.Utils.BiMap
9 (Function)Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
10 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
SingletonRecordsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
singletonSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SingleVarAgda.TypeChecking.Free.Lazy
singPluralAgda.Utils.Pretty
Size 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
size 
1 (Function)Agda.Utils.Bag
2 (Function)Agda.Utils.Size
3 (Function)Agda.Termination.SparseMatrix
sizeAndBoundVarsAgda.Auto.CaseSplit
sizeBuiltinsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
SizeConstAgda.Utils.Warshall
SizeConstraintAgda.TypeChecking.SizedTypes.Solve
sizeConstraintAgda.TypeChecking.SizedTypes.Solve
sizeContextAgda.TypeChecking.SizedTypes.Solve
SizedAgda.Utils.Size
sizedTextAgda.Utils.Pretty
SizedThing 
1 (Type/Class)Agda.Utils.Size
2 (Data Constructor)Agda.Utils.Size
sizedThingAgda.Utils.Size
sizedTypesOptionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SizeExpr 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.Utils.Warshall
sizeExprAgda.TypeChecking.SizedTypes.Solve
SizeExpr'Agda.TypeChecking.SizedTypes.Syntax
sizeHypIdsAgda.TypeChecking.SizedTypes.Solve
sizeHypothesesAgda.TypeChecking.SizedTypes.Solve
SizeInfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeLtSatAgda.Interaction.Base
sizeMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeMaxViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeMaxViewAgda.TypeChecking.SizedTypes
SizeMaxView'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
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
sizeRigidAgda.Utils.Warshall
sizeSortAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeSucAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeSucAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeSucNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeSuc_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeThingAgda.Utils.Size
sizeTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeType_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeUnivAgda.Syntax.Internal
sizeUnivAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeVarAgda.Utils.Warshall
SizeViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeViewComparableAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewComparableAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewComparableWithMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewOffsetAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewPredAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewSuc_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
Skip 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Compiler.Backend
skipAgda.Syntax.Parser.LexActions
skipBlockAgda.Syntax.Parser.Comments
SleepingConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
slowNormaliseArgsAgda.TypeChecking.Reduce
slowReduceTermAgda.TypeChecking.Reduce
sMainMetaAgda.Auto.Convert
smallestAgda.TypeChecking.SizedTypes.WarshallSolver
SmallSetAgda.Utils.SmallSet
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.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class)Agda.Utils.Warshall
SolutionsAgda.Auto.Auto
solveAgda.Utils.Warshall
solveAwakeConstraintsAgda.TypeChecking.Constraints
solveAwakeConstraints'Agda.TypeChecking.Constraints
solveClusterAgda.TypeChecking.SizedTypes.Solve
solveConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
solveConstraintTCMAgda.TypeChecking.Constraints
solveConstraint_Agda.TypeChecking.Constraints
SolvedButOpenHolesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
solveGraphAgda.TypeChecking.SizedTypes.WarshallSolver
solveGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
solveInstantiatedGoalsAgda.Interaction.InteractionTop
solveSizeConstraintsAgda.TypeChecking.SizedTypes.Solve
solveSizeConstraints_Agda.TypeChecking.SizedTypes.Solve
solveSomeAwakeConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
solveSomeAwakeConstraintsTCMAgda.TypeChecking.Constraints
solvingProblemAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
solvingProblemsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
Some 
1 (Type/Class)Agda.Utils.IndexedList
2 (Data Constructor)Agda.Utils.IndexedList
some1Agda.Utils.List1
SomeGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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 (Data Constructor)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
4 (Type/Class)Agda.Syntax.Internal
5 (Data Constructor)Agda.Syntax.Internal
6 (Type/Class)Agda.Syntax.Reflected
7 (Data Constructor)Agda.Syntax.Reflected
sort 
1 (Function)Agda.Utils.List1
2 (Function)Agda.TypeChecking.Substitute
Sort'Agda.Syntax.Internal
sortByAgda.Utils.List1
SortCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sortDefsAgda.Compiler.Common
sortedAgda.Utils.List
sortFitsInAgda.TypeChecking.Sort
SortHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sortInteractionPointsAgda.Interaction.InteractionTop
SortKit 
1 (Type/Class)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
2 (Data Constructor)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
sortKitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
sortOfAgda.TypeChecking.Sort
SortOfSplitVarErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sortOfTypeAgda.TypeChecking.Sort
sortRulesOfSymbolAgda.TypeChecking.Rewriting.Confluence
sortWithAgda.Utils.List1
Source 
1 (Type/Class)Agda.Interaction.Imports
2 (Data Constructor)Agda.Interaction.Imports
sourceAgda.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
SourceToModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sourceToModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SpaceAgda.Compiler.JS.Pretty
space 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
spanAgda.Utils.List1
spanAllowedBeforeModuleAgda.Syntax.Concrete
spanEndAgda.Utils.List
spanJustAgda.Utils.List
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.Compiler.Backend, Agda.TypeChecking.Monad
SpeculateAbortAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SpeculateCommitAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
speculateMetasAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
SpeculateResultAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
speculateTCStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
speculateTCState_Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
splitClausesAgda.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.Compiler.Backend, Agda.TypeChecking.Monad
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
splitExactlyAtAgda.Utils.List
splitExcludedLitsAgda.TypeChecking.Coverage.Match
splitLastAgda.TypeChecking.Coverage
splitLazyAgda.TypeChecking.Coverage.SplitTree
SplitLitAgda.TypeChecking.Coverage.SplitTree
splitOffTrailingWithPatternsAgda.Syntax.Abstract.Pattern
splitOnAgda.TypeChecking.CompiledClause.Compile
splitOnDotsAgda.Syntax.Parser.Parser
SplitOnIrrelevantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SplitOnNonEtaRecordAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SplitOnNonVariableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SplitOnUnusableCohesionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Irrelevance
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
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, Agda.TypeChecking.Primitive.Base
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.Compiler.Backend, Agda.TypeChecking.Monad
StackAgda.TypeChecking.CompiledClause.Match
stAgdaLibFilesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
standardOptionsAgda.Interaction.Options
standardOptions_Agda.Interaction.Options
stAreWeCachingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
starPAgda.Utils.Parser.MemoisedCPS
StarSemiRingAgda.Utils.SemiRing
startPosAgda.Syntax.Position
startPos'Agda.Syntax.Position
stateTCLensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stateTCLensMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StaticPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
StatisticsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
stBackendsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stBenchmarkAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stBuiltinThingsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stConsideringInstanceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stCurrentModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stDecodedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StdErrAgda.TypeChecking.Unquote
StdInAgda.TypeChecking.Unquote
stDirtyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stDisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StdOutAgda.TypeChecking.Unquote
stealConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
stealConstraintsTCMAgda.TypeChecking.Constraints
sTextCAgda.TypeChecking.Serialise.Base
sTextDAgda.TypeChecking.Serialise.Base
sTextEAgda.TypeChecking.Serialise.Base
stForeignCodeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshCheckpointIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshIntAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshInteractionIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshMetaIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshMutualIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshNameIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshProblemIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedBuiltinsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedDisplayFormsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedInstanceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedPartialDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedUserWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportsDisplayFormsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInstanceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInstantiateBlockingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInteractionOutputCallbackAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInteractionPointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLoadedFileCacheAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLocalBuiltinsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLocalPartialDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLocalUserWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stMetaStoreAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stModuleToSourceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StmtAgda.Utils.Haskell.Syntax
stMutualBlocksAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stOccursCheckDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
storeCachedAgdaLibFileAgda.Interaction.Library.Base
storeCachedProjectConfigAgda.Interaction.Library.Base
storeDecodedModuleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
storeDisambiguatedConstructorAgda.Interaction.Highlighting.Generate
storeDisambiguatedProjectionAgda.Interaction.Highlighting.Generate
stPatternSynImportsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPatternSynsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistBackendsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistentOptionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistentStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistLoadedFileCacheAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostAreWeCachingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostAwakeConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostConsideringInstanceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostCurrentModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostDirtyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostDisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshCheckpointIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshIntAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshMetaIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshMutualIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshNameIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshProblemIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostImportsDisplayFormsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostInstanceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostInstantiateBlockingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostInteractionPointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostLocalBuiltinsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostLocalPartialDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostMetaStoreAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostMutualBlocksAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostOccursCheckDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostponeInstanceSearchAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostPostponeInstanceSearchAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostScopeStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostShadowingNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostSignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostSleepingConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostStatisticsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostSyntaxInfoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostTCWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostUsedNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreAgdaLibFilesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreForeignCodeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreFreshInteractionIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedBuiltinsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedDisplayFormsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedInstanceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedPartialDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedUserWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreLocalUserWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreModuleToSourceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPrePatternSynImportsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPrePatternSynsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPrePragmaOptionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreProjectConfigsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreScopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreScopeStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreTokensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreVisitedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreWarningOnImportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stProjectConfigsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StrengthenAgda.Syntax.Internal, Agda.TypeChecking.Substitute
strengthenAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
strengthenSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
StrictAgda.Utils.Haskell.Syntax
StrictnessAgda.Utils.Haskell.Syntax
StrictPosAgda.TypeChecking.Positivity.Occurrence
StrictSplitAgda.TypeChecking.Coverage.SplitTree
String 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
4 (Data Constructor)Agda.Interaction.JSON
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
stripConstraintPidsAgda.Interaction.BasicOps
stripDontCareAgda.Syntax.Internal
stripNoNamesAgda.Syntax.Scope.Monad
stripPrefixByAgda.Utils.List
stripReversedSuffixAgda.Utils.List
stripRTSAgda.Interaction.Options
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.Compiler.Backend, Agda.TypeChecking.Monad
stShadowingNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stSignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stSleepingConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stStatisticsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stSyntaxInfoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stTCWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stTokensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StuckOnAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stuckOnAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stUsedNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stVisitedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stWarningOnImportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Style 
1 (Data Constructor)Agda.Utils.Pretty
2 (Type/Class)Agda.Utils.Pretty
styleAgda.Utils.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.TypeChecking.SizedTypes.Syntax
2 (Function)Agda.Compiler.JS.Substitution
3 (Function)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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
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
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 (Type/Class)Agda.Syntax.Parser.Tokens
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
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
SyntaxAgda.Syntax.Concrete
SyntaxBindingLambdaAgda.Syntax.Concrete
syntaxOfAgda.Syntax.Notation
System 
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
systemClausesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
systemTelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad