Agda-2.6.1.3: 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.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagEta_Agda.Interaction.Options.Warnings
SafeFlagInjectiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagInjective_Agda.Interaction.Options.Warnings
SafeFlagNoCoverageCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNoCoverageCheck_Agda.Interaction.Options.Warnings
SafeFlagNonTerminatingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNonTerminating_Agda.Interaction.Options.Warnings
SafeFlagNoPositivityCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNoPositivityCheck_Agda.Interaction.Options.Warnings
SafeFlagNoUniverseCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNoUniverseCheck_Agda.Interaction.Options.Warnings
SafeFlagPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagTerminating_Agda.Interaction.Options.Warnings
SafeFlagWithoutKFlagPrimEraseEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagWithoutKFlagPrimEraseEquality_Agda.Interaction.Options.Warnings
SafeModeAgda.Interaction.Options.Lenses
safePermuteAgda.Utils.Permutation
sameCohesionAgda.Syntax.Common
sameDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sameHidingAgda.Syntax.Common
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
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.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
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
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.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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sectIsSectionAgda.Syntax.Notation
sectKindAgda.Syntax.Notation
sectLevelAgda.Syntax.Notation
sectNotationAgda.Syntax.Notation
seenUIdsAgda.Auto.Syntax
selectCAgda.Interaction.Highlighting.Precise
SelfAgda.Compiler.JS.Syntax
selfAgda.Compiler.JS.Substitution
semiAgda.Utils.Pretty
SemigroupAgda.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
Set 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
setAgda.Utils.Lens
setAbsoluteIncludePathsAgda.Interaction.Options.Lenses
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
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
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
setInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
setMatchableSymbolsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaArgInfoAgda.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
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
SetNAgda.Syntax.Concrete
setNamedArgAgda.Syntax.Common
setNamedScopeAgda.Syntax.Scope.Monad
setNameOfAgda.Syntax.Common
setNameSpaceAgda.Syntax.Scope.Base
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
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
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
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.Interaction.Highlighting.Precise
severalCAgda.Interaction.Highlighting.Precise
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.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
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.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
ShouldBePiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBeSortAgda.TypeChecking.Sort, Agda.TypeChecking.CheckInternal
ShouldEndInApplicationOfTheDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldPostponeInstanceSearchAgda.TypeChecking.InstanceArguments
shouldTryFastReduceAgda.TypeChecking.Reduce
showAAgda.Syntax.Abstract.Pretty
showATopAgda.Syntax.Abstract.Pretty
showChar'Agda.Syntax.Literal
showComputedAgda.Interaction.BasicOps
showConstraintsAgda.Interaction.CommandLine
showContextAgda.Interaction.CommandLine
showGoalsAgda.Interaction.BasicOps, Agda.Interaction.EmacsTop
ShowHeadAgda.TypeChecking.Rules.Decl
showHeadAgda.TypeChecking.Rules.Decl
ShowImplicitArgsAgda.Interaction.Base
showImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showIndexAgda.Utils.String
showInfoErrorAgda.Interaction.EmacsTop
showIrrelevantArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showMetasAgda.Interaction.CommandLine
showModuleContentsAgda.Interaction.InteractionTop
showQNameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
showScopeAgda.Interaction.CommandLine
showString'Agda.Syntax.Literal
showThousandSepAgda.Utils.String
SideconditionAgda.Auto.NarrowingSearch
siFileTypeAgda.Interaction.Imports
SigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigAbstractAgda.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
sigMNameAgda.Compiler.Common
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
siModuleAgda.Interaction.Imports
siModuleNameAgda.Interaction.Imports
SimplificationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SingleLevelAgda.TypeChecking.Level
singleLevelViewAgda.TypeChecking.Level
SinglePlusAgda.TypeChecking.Level
SingletonAgda.Utils.Singleton
singleton 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BiMap
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.Graph.AdjacencyMap.Unidirectional
9 (Function)Agda.Interaction.Highlighting.Precise
singletonCAgda.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.Utils.Pretty
siSourceAgda.Interaction.Imports
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.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.Utils.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.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.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
sizePolarityAgda.TypeChecking.Polarity
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
skipBlockAgda.Syntax.Parser.Comments
SleepingConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
slowNormaliseArgsAgda.TypeChecking.Reduce
slowReduceTermAgda.TypeChecking.Reduce
sMainMetaAgda.Auto.Convert
smallestAgda.TypeChecking.SizedTypes.WarshallSolver
smallestPosAgda.Interaction.Highlighting.Precise
smallestPosCAgda.Interaction.Highlighting.Precise
SmallSetAgda.Utils.SmallSet
smashTelAgda.Syntax.Concrete.Pretty
sMetasAgda.Auto.Convert
snd3Agda.Utils.Tuple
snocAgda.Utils.List
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.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
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
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
SomeGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SomeKindsOfNamesAgda.Syntax.Scope.Base
someKindsOfNamesAgda.Syntax.Scope.Base
SomeWarningsAgda.Interaction.Imports
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
sortAgda.Syntax.Internal
Sort'Agda.Syntax.Internal
SortCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortDefsAgda.Compiler.Common
sortedAgda.Utils.List
sortFitsInAgda.TypeChecking.Sort
SortHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortInteractionPointsAgda.Interaction.InteractionTop
sortOfAgda.TypeChecking.Sort
sourceAgda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
SourceFile 
1 (Type/Class)Agda.Interaction.FindFile
2 (Data Constructor)Agda.Interaction.FindFile
SourceInfo 
1 (Type/Class)Agda.Interaction.Imports
2 (Data Constructor)Agda.Interaction.Imports
sourceInfoAgda.Interaction.Imports
sourceNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
SourceToModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sourceToModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
spaceAgda.Utils.Pretty
spanAllowedBeforeModuleAgda.Syntax.Concrete
spanEndAgda.Utils.List
spanJustAgda.Utils.List
SpecialCharacters 
1 (Type/Class)Agda.Syntax.Concrete.Pretty
2 (Data Constructor)Agda.Syntax.Concrete.Pretty
specialCharactersAgda.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
splashScreenAgda.Interaction.CommandLine
spLhsDefNameAgda.Syntax.Abstract
spLhsInfoAgda.Syntax.Abstract
spLhsPatsAgda.Syntax.Abstract
splitApplyElimsAgda.Syntax.Internal
splitArgAgda.TypeChecking.Coverage.SplitTree
SplitAtAgda.TypeChecking.Coverage.SplitTree
splitAtCAgda.Interaction.Highlighting.Precise
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.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
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.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnNonVariableAgda.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.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
srcNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
SResAgda.Auto.NarrowingSearch
sShowImplicitArgumentsAgda.Interaction.Response
sSizeUnivAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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
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
stCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDirtyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stealConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stealConstraintsTCMAgda.TypeChecking.Constraints
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
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
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
stMetaStoreAgda.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
stOccursCheckDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeDisambiguatedNameAgda.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
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
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
stPostMetaStoreAgda.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
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
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
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
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
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
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
Str 
1 (Type/Class)Agda.Utils.String
2 (Data Constructor)Agda.Utils.String
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
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
strMsgAgda.Utils.Except
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
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
StuckOnAgda.Syntax.Internal
stuckOnAgda.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 (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
subscriptAllowedAgda.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
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
SubstWithOriginAgda.TypeChecking.DisplayForm
substWithOriginAgda.TypeChecking.DisplayForm
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
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
supremumAgda.Termination.Order
supSizeAgda.Termination.SparseMatrix
swapAgda.Utils.Tuple
swap01Agda.TypeChecking.Abstract
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.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