A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
%
&
+
.
/
<
=
>
^
|
-
_
All

Index - S

S
1 (Type/Class)	Agda.TypeChecking.Serialise.Base
2 (Type/Class)	Agda.Auto.Convert
3 (Data Constructor)	Agda.Auto.Convert
SafeFlagNonTerminating	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagNoPositivityCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagPolarity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagPostulate	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagPragma	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagPrimTrustMe	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagTerminating	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeMode	Agda.Interaction.Options.Lenses
safePermute	Agda.Utils.Permutation
Same	Agda.Compiler.Epic.Injection
sameDef	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
sameVars	Agda.TypeChecking.Conversion
sanityCheckSubst	Agda.Syntax.Internal.SanityCheck
sanityCheckVars	Agda.Syntax.Internal.SanityCheck
sat
1 (Function)	Agda.Utils.Parser.MemoisedCPS
2 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
sat'	Agda.Syntax.Concrete.Operators.Parser
satisfy	Agda.Utils.Parser.ReadP
sccDAG	Agda.Utils.Graph.AdjacencyMap.Unidirectional
sccDAG'	Agda.Utils.Graph.AdjacencyMap.Unidirectional
sccomcount	Agda.Auto.NarrowingSearch
sccs	Agda.Utils.Graph.AdjacencyMap.Unidirectional
sccs'	Agda.Utils.Graph.AdjacencyMap.Unidirectional
scflip	Agda.Auto.NarrowingSearch
sChecked	Agda.Interaction.Response
SClause	Agda.TypeChecking.Coverage
scModuleParameterSub	Agda.TypeChecking.Coverage
sConsts	Agda.Auto.Convert
Scope
1 (Type/Class)	Agda.Utils.Warshall
2 (Type/Class)	Agda.Syntax.Scope.Base
3 (Data Constructor)	Agda.Syntax.Scope.Base
ScopeCheckDeclaration	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCheckExpr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCheckImport	Agda.Interaction.Imports
ScopeCheckLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCopyInfo
1 (Type/Class)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Syntax.Abstract
scopeCurrent	Agda.Syntax.Scope.Base
scopeDatatypeModule	Agda.Syntax.Scope.Base
ScopedDecl	Agda.Syntax.Abstract
ScopedExpr	Agda.Syntax.Abstract
scopedExpr	Agda.TypeChecking.Rules.Term
scopeImports	Agda.Syntax.Scope.Base
ScopeInfo
1 (Type/Class)	Agda.Syntax.Scope.Base
2 (Data Constructor)	Agda.Syntax.Scope.Base
scopeInScope	Agda.Syntax.Scope.Base
scopeInverseModule	Agda.Syntax.Scope.Base
scopeInverseName	Agda.Syntax.Scope.Base
scopeLocals	Agda.Syntax.Scope.Base
scopeLookup	Agda.Syntax.Scope.Base
scopeLookup'	Agda.Syntax.Scope.Base
ScopeM	Agda.Syntax.Scope.Monad
ScopeMemo
1 (Type/Class)	Agda.Syntax.Scope.Monad
2 (Data Constructor)	Agda.Syntax.Scope.Monad
scopeModules	Agda.Syntax.Scope.Base
scopeName	Agda.Syntax.Scope.Base
scopeNameSpace	Agda.Syntax.Scope.Base
ScopeNameSpaces	Agda.Syntax.Scope.Base
scopeNameSpaces	Agda.Syntax.Scope.Base
scopeParents	Agda.Syntax.Scope.Base
scopePrecedence	Agda.Syntax.Scope.Base
Scoping	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
scPats	Agda.TypeChecking.Coverage
scsub1	Agda.Auto.NarrowingSearch
scsub2	Agda.Auto.NarrowingSearch
scSubst	Agda.TypeChecking.Coverage
scTarget	Agda.TypeChecking.Coverage
scTel	Agda.TypeChecking.Coverage
sCurMeta	Agda.Auto.Convert
searchAbout	Agda.Interaction.InteractionTop
secondPart	Agda.TypeChecking.Telescope
secTelescope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Section
1 (Data Constructor)	Agda.Syntax.Abstract
2 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SectionApp
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
Sections	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sectIsSection	Agda.Syntax.Fixity
sectKind	Agda.Syntax.Fixity
sectLevel	Agda.Syntax.Fixity
sectNotation	Agda.Syntax.Fixity
selectC	Agda.Interaction.Highlighting.Precise
Self	Agda.Compiler.JS.Syntax
self	Agda.Compiler.JS.Substitution
semi	Agda.Utils.Pretty
SemiRing	Agda.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
sepBy	Agda.Utils.Parser.ReadP
sepBy1	Agda.Utils.Parser.ReadP
SeqArg
1 (Type/Class)	Agda.Compiler.Treeless.Subst
2 (Data Constructor)	Agda.Compiler.Treeless.Subst
seqc	Agda.Auto.NarrowingSearch
seqctx	Agda.Auto.CaseSplit
seqPO	Agda.Utils.PartialOrd
sEqs	Agda.Auto.Convert
Serialization	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Serialize	Agda.Compiler.UHC.Bridge
serialize	Agda.Compiler.UHC.Bridge
Set
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Auto.Syntax
set	Agda.Utils.Lens
setAbsoluteIncludePaths	Agda.Interaction.Options.Lenses
setArgInfo	Agda.Syntax.Common
setArgOccurrences	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setBenchmarking	Agda.Utils.Benchmark
setBuiltinThings	Agda.TypeChecking.Monad.Builtin
setCommandLineOptions
1 (Function)	Agda.Interaction.Options.Lenses
2 (Function)	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setCommandLineOptions'	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setCommandLineOpts	Agda.Interaction.InteractionTop
setCompiledArgUse	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setConName	Agda.Syntax.Internal
setContextPrecedence	Agda.Syntax.Scope.Monad
setCurrentModule	Agda.Syntax.Scope.Monad
setCurrentRange	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
setDecodedModules	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
setDefaultModuleParameters	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setErasedConArgs	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setEtaEquality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setFoldl	Agda.TypeChecking.SizedTypes.WarshallSolver
setFunctionFlag	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setHiding	Agda.Syntax.Common
setImportedName	Agda.Syntax.Common
setIncludeDirs	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setIncludePaths	Agda.Interaction.Options.Lenses
setInput	Agda.Syntax.Parser.LookAhead
setInputFile	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInteractionOutputCallback	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setInterface	Agda.Compiler.Common
setIntervalFile	Agda.Syntax.Position
setLastPos	Agda.Syntax.Parser.Monad
setLexInput	Agda.Syntax.Parser.Alex
setLibraryIncludes	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setLibraryPaths	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setLocalVars	Agda.Syntax.Scope.Monad
setMetaNameSuggestion	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
setMutual	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
setMutualBlockInfo	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
SetN	Agda.Syntax.Concrete
setNamedScope	Agda.Syntax.Scope.Monad
setNameSpace	Agda.Syntax.Scope.Base
SetOmegaNotValidType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setOptionsFromPragma	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setOrigin	Agda.Syntax.Common
setParsePos	Agda.Syntax.Parser.Monad
setPatternSyns	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setPersistentVerbosity	Agda.Interaction.Options.Lenses
setPolarity	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setPragmaOptions
1 (Function)	Agda.Interaction.Options.Lenses
2 (Function)	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setPrevToken	Agda.Syntax.Parser.Monad
setPtr	Agda.Utils.Pointer, Agda.Syntax.Internal
SetRange
1 (Type/Class)	Agda.Syntax.Position
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setRange	Agda.Syntax.Position
setRelevance	Agda.Syntax.Common
SetS	Agda.Syntax.Reflected
setSafeMode	Agda.Interaction.Options.Lenses
setScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setScopeAccess	Agda.Syntax.Scope.Base
setScopeLocals	Agda.Syntax.Scope.Base
setSignature	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setTag
1 (Function)	Agda.Compiler.UHC.Pragmas.Base, Agda.Compiler.UHC.Pragmas.Parse
2 (Function)	Agda.Compiler.Epic.Injection
setTerminates	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
SetToInfty	Agda.TypeChecking.SizedTypes.WarshallSolver
setToInfty	Agda.TypeChecking.SizedTypes.WarshallSolver
setTopLevelModule	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setTreeless	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setValueMetaName	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
setVerbosity	Agda.Interaction.Options.Lenses
setVisitedModules	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
several	Agda.Interaction.Highlighting.Precise
severalC	Agda.Interaction.Highlighting.Precise
sgListT	Agda.Utils.ListT
sgMListT	Agda.Utils.ListT
SgTel	Agda.Syntax.Internal
sgTel	Agda.Syntax.Internal
ShadowedModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShadowedVar	Agda.Syntax.Scope.Base
shadowLocal	Agda.Syntax.Scope.Base
Shared	Agda.Syntax.Internal
shared	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
sharedFun	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
sharedType	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
shared_	Agda.Syntax.Internal
sharing	Agda.Utils.Update
shift	Agda.Compiler.JS.Substitution
shifter	Agda.Compiler.JS.Substitution
shiftFrom	Agda.Compiler.JS.Substitution
ShouldBeApplicationOf	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeAppliedToTheDatatypeParameters	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeASort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeEmpty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBePi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeRecordPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeRecordType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldEndInApplicationOfTheDatatype	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
showA	Agda.Syntax.Abstract.Pretty
showATop	Agda.Syntax.Abstract.Pretty
showChar'	Agda.Syntax.Literal
showComparison	Agda.Interaction.BasicOps
showComputed	Agda.Interaction.BasicOps
showConstraints	Agda.Interaction.CommandLine
showContext	Agda.Interaction.CommandLine
ShowHead	Agda.TypeChecking.Rules.Decl
showHead	Agda.TypeChecking.Rules.Decl
ShowImplicitArgs	Agda.Interaction.InteractionTop
showImplicitArguments	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showIndex	Agda.Utils.String
showIrrelevantArguments	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showMetas	Agda.Interaction.CommandLine
showModuleContents	Agda.Interaction.InteractionTop
showOpenMetas	Agda.Interaction.InteractionTop
showQNameId	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
showScope	Agda.Interaction.CommandLine
showString'	Agda.Syntax.Literal
showThousandSep	Agda.Utils.String
Sidecondition	Agda.Auto.NarrowingSearch
Sig	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigDefinitions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigMName	Agda.Compiler.Common
Signature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigRewriteRules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigSections	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Simplification	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Simplified	Agda.Interaction.BasicOps
Simplify	Agda.TypeChecking.Reduce
simplify	Agda.TypeChecking.Reduce
simplify'	Agda.TypeChecking.Reduce
simplify1	Agda.TypeChecking.SizedTypes.Syntax
simplifyBlocked'	Agda.TypeChecking.Reduce
simplifyLevelConstraint	Agda.TypeChecking.LevelConstraints
simplifyTTerm	Agda.Compiler.Treeless.Simplify
simplifyWithHypotheses	Agda.TypeChecking.SizedTypes.WarshallSolver
singleConstructorType	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
Singleton	Agda.Utils.Singleton
singleton
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Singleton
4 (Function)	Agda.Utils.BiMap
5 (Function)	Agda.Utils.Bag
6 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function)	Agda.Utils.Trie
8 (Function)	Agda.Interaction.Highlighting.Precise
singletonC	Agda.Interaction.Highlighting.Precise
SingletonRecords	Agda.TypeChecking.MetaVars
singletonS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SingleVar	Agda.TypeChecking.Free.Lazy
Size
1 (Type/Class)	Agda.Termination.SparseMatrix
2 (Data Constructor)	Agda.Termination.SparseMatrix
size
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Bag
3 (Function)	Agda.Utils.Size
4 (Function)	Agda.Termination.SparseMatrix
SizeConst	Agda.Utils.Warshall
SizeConstraint	Agda.TypeChecking.SizedTypes.Solve
sizeConstraint	Agda.TypeChecking.SizedTypes.Solve
sizeContext	Agda.TypeChecking.SizedTypes.Solve
Sized	Agda.Utils.Size
sizedText	Agda.Utils.Pretty
SizedThing
1 (Type/Class)	Agda.Utils.Size
2 (Data Constructor)	Agda.Utils.Size
sizedThing	Agda.Utils.Size
SizeExpr
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.Utils.Warshall
sizeExpr	Agda.TypeChecking.SizedTypes.Solve
SizeExpr'	Agda.TypeChecking.SizedTypes.Syntax
sizeHypIds	Agda.TypeChecking.SizedTypes.Solve
sizeHypotheses	Agda.TypeChecking.SizedTypes.Solve
SizeInf	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeLtSat	Agda.Interaction.BasicOps
sizeMax	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeMaxView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeMaxView	Agda.TypeChecking.SizedTypes
SizeMeta
1 (Data Constructor)	Agda.TypeChecking.SizedTypes
2 (Type/Class)	Agda.TypeChecking.SizedTypes.Solve
3 (Data Constructor)	Agda.TypeChecking.SizedTypes.Solve
sizeMetaArgs	Agda.TypeChecking.SizedTypes.Solve
sizeMetaId	Agda.TypeChecking.SizedTypes.Solve
sizePolarity	Agda.TypeChecking.Polarity
sizeRigid	Agda.Utils.Warshall
sizeSort	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeSuc	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSuc	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSucName	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSuc_	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeThing	Agda.Utils.Size
sizeType	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeType_	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeUniv	Agda.Syntax.Internal
sizeUniv	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeVar	Agda.Utils.Warshall
SizeView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeViewComparable	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewComparable	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewComparableWithMax	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewOffset	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewPred	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewSuc_	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
Skip	Agda.Auto.Syntax
skipBlock	Agda.Syntax.Parser.Comments
skipMany	Agda.Utils.Parser.ReadP
skipMany1	Agda.Utils.Parser.ReadP
skipSpaces	Agda.Utils.Parser.ReadP
SleepingConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
slowReduceTerm	Agda.TypeChecking.Reduce
sLub	Agda.TypeChecking.Substitute
sMainMeta	Agda.Auto.Convert
Small	Agda.Syntax.Common
smallest	Agda.TypeChecking.SizedTypes.WarshallSolver
smallestPos	Agda.Interaction.Highlighting.Precise
smallestPosC	Agda.Interaction.Highlighting.Precise
smallParams	Agda.TypeChecking.Rules.Data
smash'em	Agda.Compiler.Epic.Smashing
smashable	Agda.Compiler.Epic.Smashing
smashTel	Agda.Syntax.Concrete.Pretty
sMetas	Agda.Auto.Convert
snd3	Agda.Utils.Tuple
Sol	Agda.Auto.CaseSplit
Solution
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.Utils.Warshall
solve
1 (Function)	Agda.Utils.Warshall
2 (Function)	Agda.Compiler.Epic.Injection
solveAwakeConstraints	Agda.TypeChecking.Constraints
solveAwakeConstraints'	Agda.TypeChecking.Constraints
solveCluster	Agda.TypeChecking.SizedTypes.Solve
solveConstraint	Agda.TypeChecking.Constraints
solveConstraint_	Agda.TypeChecking.Constraints
SolvedButOpenHoles	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
solveGraph	Agda.TypeChecking.SizedTypes.WarshallSolver
solveGraphs	Agda.TypeChecking.SizedTypes.WarshallSolver
solveInstantiatedGoals	Agda.Interaction.InteractionTop
solveSizeConstraints	Agda.TypeChecking.SizedTypes.Solve
solveSizeConstraints_	Agda.TypeChecking.SizedTypes.Solve
solvingProblem	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
solvingProblems	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
SomeWarnings	Agda.Interaction.Imports
SomeWhere	Agda.Syntax.Concrete
Sort
1 (Type/Class)	Agda.Syntax.Reflected
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
4 (Type/Class)	Agda.Syntax.Internal
5 (Data Constructor)	Agda.Syntax.Internal
6 (Data Constructor)	Agda.Auto.Syntax
7 (Type/Class)	Agda.Auto.Syntax
sort	Agda.Syntax.Internal
SortCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortDefs	Agda.Compiler.Common
sorted	Agda.Utils.List
SortHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortInteractionPoints	Agda.Interaction.InteractionTop
sortOfConst	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
sortTm	Agda.TypeChecking.Substitute
source	Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
sourceNodes	Agda.Utils.Graph.AdjacencyMap.Unidirectional
SourceToModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sourceToModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
space	Agda.Utils.Pretty
spanAllowedBeforeModule	Agda.Syntax.Concrete
spanJust	Agda.Utils.List
Specified	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SpineClause	Agda.Syntax.Abstract
SpineLHS
1 (Type/Class)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Syntax.Abstract
spineToLhs	Agda.Syntax.Abstract
spineToLhsCore	Agda.Syntax.Abstract
splashScreen	Agda.Interaction.CommandLine
spLhsDefName	Agda.Syntax.Abstract
spLhsInfo	Agda.Syntax.Abstract
spLhsPats	Agda.Syntax.Abstract
spLhsWithPats	Agda.Syntax.Abstract
Split	Agda.TypeChecking.Rules.LHS.Problem
splitApplyElims	Agda.Syntax.Internal
splitArg	Agda.TypeChecking.Coverage.SplitTree
SplitAt	Agda.TypeChecking.Coverage.SplitTree
splitAtC	Agda.Interaction.Highlighting.Precise
splitBindings	Agda.TypeChecking.Coverage.SplitTree
splitC	Agda.TypeChecking.CompiledClause.Compile
SplitClause	Agda.TypeChecking.Coverage
splitClauses	Agda.TypeChecking.Coverage
splitClauseWithAbsurd	Agda.TypeChecking.Coverage
splitCommas	Agda.Interaction.Library.Parse
SplitError
1 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
splitExactlyAt	Agda.Utils.List
splitFocus	Agda.TypeChecking.Rules.LHS.Problem
splitLast	Agda.TypeChecking.Coverage
splitLPats	Agda.TypeChecking.Rules.LHS.Problem
splitOn	Agda.TypeChecking.CompiledClause.Compile
splitOnDots	Agda.Syntax.Parser.Parser
SplitOnIrrelevant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
splitPerm	Agda.TypeChecking.Telescope
SplitProblem	Agda.TypeChecking.Rules.LHS.Problem
splitProblem	Agda.TypeChecking.Rules.LHS.Split
splitProjection	Agda.TypeChecking.Rules.LHS.Problem
splitProjOrigin	Agda.TypeChecking.Rules.LHS.Problem
SplitRest	Agda.TypeChecking.Rules.LHS.Problem
splitRestType	Agda.TypeChecking.Rules.LHS.Problem
splitResult	Agda.TypeChecking.Coverage
splitRPats	Agda.TypeChecking.Rules.LHS.Problem
splitS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SplitTel
1 (Type/Class)	Agda.TypeChecking.Telescope
2 (Data Constructor)	Agda.TypeChecking.Telescope
splitTelescope	Agda.TypeChecking.Telescope
splitTelescopeExact	Agda.TypeChecking.Telescope
splitTelForWith	Agda.TypeChecking.With
SplittingDone	Agda.TypeChecking.Coverage.SplitTree
SplitTree	Agda.TypeChecking.Coverage.SplitTree
SplitTree'	Agda.TypeChecking.Coverage.SplitTree
SplitTreeLabel
1 (Type/Class)	Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor)	Agda.TypeChecking.Coverage.SplitTree
SplitTrees	Agda.TypeChecking.Coverage.SplitTree
splitTrees	Agda.TypeChecking.Coverage.SplitTree
SplitTrees'	Agda.TypeChecking.Coverage.SplitTree
square	Agda.Termination.SparseMatrix
src	Agda.TypeChecking.SizedTypes.WarshallSolver
SrcFile	Agda.Syntax.Position
srcFile	Agda.Syntax.Position
srcNodes	Agda.Utils.Graph.AdjacencyMap.Unidirectional
SRes	Agda.Auto.NarrowingSearch
sShowImplicitArguments	Agda.Interaction.Response
sSizeUniv	Agda.TypeChecking.Primitive
sSuc	Agda.Syntax.Internal
St
1 (Type/Class)	Agda.TypeChecking.Serialise.Base
2 (Data Constructor)	Agda.TypeChecking.Serialise.Base
stAccumStatistics	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Stack	Agda.TypeChecking.CompiledClause.Match
standardOptions	Agda.Interaction.Options
standardOptions_	Agda.Interaction.Options
StarSemiRing	Agda.Utils.SemiRing
startPos	Agda.Syntax.Position
startPos'	Agda.Syntax.Position
StaticPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
Statistics	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stats	Agda.TypeChecking.Serialise.Base
Status
1 (Type/Class)	Agda.Interaction.Response
2 (Data Constructor)	Agda.Interaction.Response
status	Agda.Interaction.InteractionTop
stAwakeConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stBenchmark	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stBuiltinThings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stCurrentModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stDecodedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stDirty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stDisambiguatedNames	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stealConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
step	Agda.Compiler.Epic.Erasure
stFreshCtxId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshInt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshInteractionId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshMetaId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshMutualId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshNameId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshProblemId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellCode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellImportsUHC	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedBuiltins	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedDisplayForms	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedInstanceDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportsDisplayForms	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInstanceDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionOutputCallback	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stLoadedFileCache	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stLocalBuiltins	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMetaStore	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stModuleParameters	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stModuleToSource	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Stmt	Agda.Utils.Haskell.Syntax
stMutualBlocks	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stOccursCheckDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
storeDecodedModule	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
storeDisambiguatedName	Agda.Interaction.Highlighting.Generate
stPatternSynImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPatternSyns	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPersistentOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPersistentState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostAwakeConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostCurrentModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostDirty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostDisambiguatedNames	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostFreshCtxId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostFreshInt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostFreshMetaId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostFreshMutualId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostFreshNameId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostFreshProblemId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostImportsDisplayForms	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostInstanceDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostInteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostLocalBuiltins	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostMetaStore	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostModuleParameters	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostMutualBlocks	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostOccursCheckDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostScopeState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostSignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostSleepingConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostSolvedInteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostStatistics	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostSyntaxInfo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPostTCWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPragmaOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreFreshInteractionId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreHaskellCode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreHaskellImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreHaskellImportsUHC	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreImportedBuiltins	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreImportedDisplayForms	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreImportedInstanceDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreImportedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreModuleToSource	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPrePatternSynImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPrePatternSyns	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPrePragmaOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreScopeState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreTokens	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPreVisitedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Str
1 (Type/Class)	Agda.Utils.String
2 (Data Constructor)	Agda.Utils.String
Strengthen	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
strengthen	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
strengthenS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
StrictPos	Agda.TypeChecking.Positivity.Occurrence
String
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Data Constructor)	Agda.Compiler.JS.Syntax
string	Agda.Utils.Parser.ReadP
stringC	Agda.TypeChecking.Serialise.Base
stringD	Agda.TypeChecking.Serialise.Base
stringE	Agda.TypeChecking.Serialise.Base
stringNameParts	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
stringParts	Agda.Syntax.Notation
stringToArgName	Agda.Syntax.Internal
stringToMyId	Agda.Auto.Syntax
stringToRawName	Agda.Syntax.Common
stripComments	Agda.Interaction.Library.Parse
stripDontCare	Agda.Syntax.Internal
stripNoNames	Agda.Syntax.Scope.Monad
stripPrefixBy	Agda.Utils.List
stripUnusedArguments	Agda.Compiler.Treeless.Unused
stripWithClausePatterns	Agda.TypeChecking.With
strMsg	Agda.Utils.Except
strongly	Agda.TypeChecking.MetaVars.Occurs
StronglyRigid
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy
2 (Data Constructor)	Agda.TypeChecking.Free.Old
3 (Data Constructor)	Agda.TypeChecking.Free
4 (Data Constructor)	Agda.TypeChecking.MetaVars.Occurs
stronglyRigidVars
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
StrPart	Agda.TypeChecking.Unquote
stScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSleepingConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSolvedInteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stStatistics	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSyntaxInfo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTCWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTokens	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
StuckOn	Agda.Syntax.Internal
stuckOn	Agda.Syntax.Internal
stVisitedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Style
1 (Data Constructor)	Agda.Utils.Pretty
2 (Type/Class)	Agda.Utils.Pretty
style	Agda.Utils.Pretty
Sub
1 (Type/Class)	Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)	Agda.Auto.Syntax
sub	Agda.Auto.Syntax
SubConstraints
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
subi	Agda.Auto.Syntax
subLevel	Agda.TypeChecking.Level
Subscript	Agda.Utils.Suffix
Subst	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subst
1 (Function)	Agda.TypeChecking.SizedTypes.Syntax
2 (Function)	Agda.Compiler.JS.Substitution
3 (Function)	Agda.Compiler.Epic.AuxAST
4 (Function)	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subst'	Agda.Compiler.JS.Substitution
substBody	Agda.TypeChecking.CompiledClause.Compile
substBranch	Agda.Compiler.Epic.AuxAST
SubstCand	Agda.TypeChecking.MetaVars
SubstExpr	Agda.Syntax.Abstract
substExpr	Agda.Syntax.Abstract
substForDot	Agda.Compiler.Epic.Injection
Substitute	Agda.TypeChecking.SizedTypes.Syntax
substituter	Agda.Compiler.JS.Substitution
Substitution
1 (Type/Class)	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
2 (Type/Class)	Agda.TypeChecking.Rules.LHS.Problem
Substitution'	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
substLit	Agda.Compiler.Epic.FromAgda
substPattern	Agda.Syntax.Abstract
substs	Agda.Compiler.Epic.AuxAST
substTerm	Agda.Compiler.Epic.FromAgda
substUnder	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subsvars	Agda.Auto.SearchControl
subtract	Agda.Utils.VarSet
subtypingForSizeLt	Agda.TypeChecking.MetaVars
sucName	Agda.TypeChecking.Level
Suffix
1 (Type/Class)	Agda.Utils.Suffix
2 (Type/Class)	Agda.Utils.List
suffixView	Agda.Utils.Suffix
Suggest	Agda.Syntax.Internal
suggest	Agda.Syntax.Internal
supremum	Agda.Termination.Order
supSize	Agda.Termination.SparseMatrix
swap	Agda.Utils.Tuple
swap01	Agda.TypeChecking.Abstract
switchBenchmarking	Agda.Utils.Benchmark
SymArrow	Agda.Syntax.Parser.Tokens
SymAs	Agda.Syntax.Parser.Tokens
SymBar	Agda.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
symbol	Agda.Syntax.Parser.LexActions
SymCloseBrace	Agda.Syntax.Parser.Tokens
SymCloseIdiomBracket	Agda.Syntax.Parser.Tokens
SymCloseParen	Agda.Syntax.Parser.Tokens
SymClosePragma	Agda.Syntax.Parser.Tokens
SymCloseVirtualBrace	Agda.Syntax.Parser.Tokens
SymColon	Agda.Syntax.Parser.Tokens
SymDot	Agda.Syntax.Parser.Tokens
SymDotDot	Agda.Syntax.Parser.Tokens
SymDoubleCloseBrace	Agda.Syntax.Parser.Tokens
SymDoubleOpenBrace	Agda.Syntax.Parser.Tokens
SymEllipsis	Agda.Syntax.Parser.Tokens
SymEndComment	Agda.Syntax.Parser.Tokens
SymEqual	Agda.Syntax.Parser.Tokens
SymLambda	Agda.Syntax.Parser.Tokens
SymOpenBrace	Agda.Syntax.Parser.Tokens
SymOpenIdiomBracket	Agda.Syntax.Parser.Tokens
SymOpenParen	Agda.Syntax.Parser.Tokens
SymOpenPragma	Agda.Syntax.Parser.Tokens
SymOpenVirtualBrace	Agda.Syntax.Parser.Tokens
SymQuestionMark	Agda.Syntax.Parser.Tokens
SymSemi	Agda.Syntax.Parser.Tokens
SymUnderscore	Agda.Syntax.Parser.Tokens
SymVirtualSemi	Agda.Syntax.Parser.Tokens
sync	Agda.Syntax.Parser.LookAhead
SynEq	Agda.TypeChecking.SyntacticEquality
Syntax	Agda.Syntax.Concrete
SyntaxBindingLambda	Agda.Syntax.Concrete
syntaxOf	Agda.Syntax.Fixity