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

Index - S

S 
1 (Type/Class)Agda.Auto.Convert
2 (Data Constructor)Agda.Auto.Convert
sameVarsAgda.TypeChecking.Conversion
sampleAgda.Utils.QuickCheck
sample'Agda.Utils.QuickCheck
satisfyAgda.Utils.ReadP
sccomcountAgda.Auto.NarrowingSearch
scflipAgda.Auto.NarrowingSearch
sCheckedAgda.Interaction.GhciTop
SClauseAgda.TypeChecking.Coverage
sConstsAgda.Auto.Convert
Scope 
1 (Type/Class)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
3 (Type/Class)Agda.Utils.Warshall
ScopeCheckDeclarationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCheckDefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCheckImportAgda.Interaction.Imports
ScopeCheckLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCurrentAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopedDeclAgda.Syntax.Abstract
ScopedDefAgda.Syntax.Abstract
ScopedExprAgda.Syntax.Abstract
scopeImportedAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeImportsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeInfo 
1 (Type/Class)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLocalsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLookupAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
scopeModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeParentsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePrecedenceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePrivateAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePublicAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scPatsAgda.TypeChecking.Coverage
scPermAgda.TypeChecking.Coverage
scsub1Agda.Auto.NarrowingSearch
scsub2Agda.Auto.NarrowingSearch
scSubstAgda.TypeChecking.Coverage
scTelAgda.TypeChecking.Coverage
sCurMetaAgda.Auto.Convert
secFreeVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
secondPartAgda.TypeChecking.Telescope
secTelescopeAgda.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
SectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
semiAgda.Utils.Pretty
SemiRing 
1 (Type/Class)Agda.Utils.SemiRing
2 (Type/Class)Agda.Termination.Semiring
Semiring 
1 (Type/Class)Agda.Termination.Semiring
2 (Data Constructor)Agda.Termination.Semiring
semiringInvariantAgda.Termination.Semiring
sep 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
sepByAgda.Utils.ReadP
sepBy1Agda.Utils.ReadP
seqcAgda.Auto.NarrowingSearch
seqctxAgda.Auto.CaseSplit
sEqsAgda.Auto.Convert
Set 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
setAgda.Syntax.Internal
set0Agda.Syntax.Internal
setArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setBuiltinThingsAgda.TypeChecking.Monad.Builtin
setCommandLineOptions 
1 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
2 (Function)Agda.Interaction.GhciTop
setContextPrecedenceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setCurrentModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setCurrentRangeAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
setDecodedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
setFreqsAgda.TypeChecking.Test.Generators
setImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setIncludeDirsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInputAgda.Syntax.Parser.LookAhead
setInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInterfaceAgda.Compiler.MAlonzo.Misc
setLastPosAgda.Syntax.Parser.Monad
setLexInputAgda.Syntax.Parser.Alex
setLocalVarsAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
SetNAgda.Syntax.Concrete
setOptionsFromPragmaAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setParsePosAgda.Syntax.Parser.Monad
setPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setPragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setPrevTokenAgda.Syntax.Parser.Monad
SetRange 
1 (Type/Class)Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
setScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setScopeAccessAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
setShowImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setVisitedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
severalAgda.Interaction.Highlighting.Precise
ShadowedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeApplicationOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeAppliedToTheDatatypeParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeASortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBePiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeRecordTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldEndInApplicationOfTheDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
shouldEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
shouldReifyInteractionPointsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showAAgda.Syntax.Abstract.Pretty
showATopAgda.Syntax.Abstract.Pretty
showChar'Agda.Syntax.Concrete.Pretty
showComparisonAgda.Interaction.BasicOps
showConstraintsAgda.Interaction.CommandLine.CommandLine
showContextAgda.Interaction.CommandLine.CommandLine
showHighlightingInfoAgda.Interaction.Highlighting.Emacs
showImplicitArgsAgda.Interaction.GhciTop
showImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showIndexAgda.Utils.String
showMetasAgda.Interaction.CommandLine.CommandLine
showModuleContentsAgda.Interaction.GhciTop
showNumIIdAgda.Interaction.GhciTop
showPatAgda.TypeChecking.With
showQNameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
showScopeAgda.Interaction.CommandLine.CommandLine
showStatusAgda.Interaction.GhciTop
showString'Agda.Syntax.Concrete.Pretty
shrinkAgda.Utils.QuickCheck
Shrink2 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
ShrinkCAgda.TypeChecking.Test.Generators
shrinkCAgda.TypeChecking.Test.Generators
Shrinking 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
shrinkingAgda.Utils.QuickCheck
shrinkInitAgda.Utils.QuickCheck
shrinkIntegralAgda.Utils.QuickCheck
shrinkNothingAgda.Utils.QuickCheck
shrinkRealFracAgda.Utils.QuickCheck
ShrinkStateAgda.Utils.QuickCheck
shrinkStateAgda.Utils.QuickCheck
SideconditionAgda.Auto.NarrowingSearch
SigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigDefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigMNameAgda.Compiler.MAlonzo.Misc
SignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigSectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
singleConstructorTypeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
singleton 
1 (Function)Agda.Utils.Graph
2 (Function)Agda.Utils.Trie
3 (Function)Agda.Interaction.Highlighting.Precise
SingletonRecordsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
Size 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
3 (Type/Class)Agda.Termination.Matrix
4 (Data Constructor)Agda.Termination.Matrix
size 
1 (Function)Agda.Utils.Size
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
4 (Function)Agda.Termination.Lexicographic
SizeConstAgda.Utils.Warshall
SizeConstraintAgda.TypeChecking.SizedTypes
SizedAgda.Utils.Size
sizedAgda.Utils.QuickCheck
SizedList 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
SizeExpr 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.SizedTypes
sizeExprAgda.TypeChecking.SizedTypes
SizeInfAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeInvariant 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
SizeMetaAgda.TypeChecking.SizedTypes
sizePolarityAgda.TypeChecking.Polarity
sizeRigidAgda.Utils.Warshall
SizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeVarAgda.Utils.Warshall
SizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SkipAgda.Auto.Syntax
skipBlockAgda.Syntax.Parser.Comments
skipManyAgda.Utils.ReadP
skipMany1Agda.Utils.ReadP
skipSpacesAgda.Utils.ReadP
sLubAgda.Syntax.Internal
sMainMetaAgda.Auto.Convert
smallestPosAgda.Interaction.Highlighting.Precise
Smart 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
smashTelAgda.Syntax.Concrete.Pretty
sMetasAgda.Auto.Convert
SolAgda.Auto.CaseSplit
SolutionAgda.Utils.Warshall
solveAgda.Utils.Warshall
solveConstraintAgda.TypeChecking.Constraints
solveConstraintsAgda.TypeChecking.Constraints
solveLevelConstraintsAgda.TypeChecking.UniversePolymorphism
solveSizeConstraintsAgda.TypeChecking.SizedTypes
SomeWhereAgda.Syntax.Concrete
Sort 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.Auto.Syntax
3 (Type/Class)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Internal
sortAgda.Syntax.Internal
SortCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortFreqAgda.TypeChecking.Test.Generators
SortFreqs 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
sortFreqsAgda.TypeChecking.Test.Generators
SortHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortInteractionPointsAgda.Interaction.GhciTop
sortOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
sourceAgda.Termination.CallGraph
SourceToModuleAgda.Interaction.FindFile
sourceToModuleAgda.Interaction.FindFile
spaceAgda.Utils.Pretty
splashScreenAgda.Interaction.CommandLine.CommandLine
SplitAgda.TypeChecking.Rules.LHS.Problem
splitAgda.TypeChecking.Coverage
split'Agda.TypeChecking.Coverage
splitCAgda.TypeChecking.CompiledClause
SplitClauseAgda.TypeChecking.Coverage
splitClauseAgda.TypeChecking.Coverage
splitClauseWithAbsAgda.TypeChecking.Coverage
SplitError 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Type/Class)Agda.TypeChecking.Coverage
splitOnAgda.TypeChecking.CompiledClause
SplitOnIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SplitPanicAgda.TypeChecking.Rules.LHS.Problem
splitPermAgda.TypeChecking.Telescope
SplitProblemAgda.TypeChecking.Rules.LHS.Problem
splitProblemAgda.TypeChecking.Rules.LHS.Split
SplitTel 
1 (Type/Class)Agda.TypeChecking.Telescope
2 (Data Constructor)Agda.TypeChecking.Telescope
splitTelescopeAgda.TypeChecking.Telescope
square 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
srcFileAgda.Syntax.Position, Agda.Interaction.GhciTop
SResAgda.Auto.NarrowingSearch
sShowImplicitArgumentsAgda.Interaction.GhciTop
sSucAgda.Syntax.Internal
StackAgda.TypeChecking.CompiledClause.Match
standardOptions_Agda.Interaction.Options
startPosAgda.Syntax.Position, Agda.Interaction.GhciTop
State 
1 (Type/Class)Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Interaction.GhciTop
StatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Status 
1 (Type/Class)Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Interaction.GhciTop
statusAgda.Interaction.GhciTop
stBuiltinThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stdArgsAgda.Utils.QuickCheck
stDecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stdoutFlushAgda.Utils.IO.Locale
stepAgda.Compiler.Epic.Erasure
stFreshThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stLocalBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stModuleToSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMutualBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
storeAgda.Utils.Pointer
storeDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
stPersistentOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Str 
1 (Type/Class)Agda.Utils.QuickCheck
2 (Data Constructor)Agda.Utils.Pretty
3 (Type/Class)Agda.TypeChecking.Primitive
4 (Data Constructor)Agda.TypeChecking.Primitive
StrictAgda.Syntax.Strict
strictAgda.Syntax.Strict
StringAgda.Interaction.Highlighting.Precise
stringAgda.Utils.ReadP
stripImplicitsAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
stripNoNamesAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
stripWithClausePatternsAgda.TypeChecking.With
stScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stStatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stVisitedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Style 
1 (Type/Class)Agda.Utils.Pretty
2 (Data Constructor)Agda.Utils.Pretty
styleAgda.Utils.Pretty
Sub 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.TypeChecking.Rules.LHS.Unify
subAgda.Auto.Syntax
SubConstraints 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
subiAgda.Auto.Syntax
SubstAgda.TypeChecking.Substitute
subst 
1 (Function)Agda.Compiler.Epic.AuxAST
2 (Function)Agda.TypeChecking.Substitute
substBranchAgda.Compiler.Epic.AuxAST
substCCAgda.Compiler.Epic.Forcing
substCCBodyAgda.Compiler.Epic.Forcing
Substitution 
1 (Type/Class)Agda.TypeChecking.Substitute
2 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
substLitAgda.Compiler.Epic.FromAgda
substsAgda.TypeChecking.Substitute
substsCCBodyAgda.Compiler.Epic.Forcing
substTermAgda.Compiler.Epic.FromAgda
substUnderAgda.TypeChecking.Substitute
subsvarsAgda.Auto.SearchControl
SucAgda.Syntax.Internal
SuccessAgda.Utils.QuickCheck
suchThatAgda.Utils.QuickCheck
suchThatMaybeAgda.Utils.QuickCheck
sucNameAgda.TypeChecking.Level
Suffix 
1 (Type/Class)Agda.Utils.Suffix
2 (Type/Class)Agda.Utils.List
suffixViewAgda.Utils.Suffix
supremumAgda.Termination.CallGraph
SymArrowAgda.Syntax.Parser.Tokens
SymAsAgda.Syntax.Parser.Tokens
SymBarAgda.Syntax.Parser.Tokens
Symbol 
1 (Type/Class)Agda.Syntax.Parser.Tokens
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
symbolAgda.Syntax.Parser.LexActions
SymCloseBraceAgda.Syntax.Parser.Tokens
SymCloseParenAgda.Syntax.Parser.Tokens
SymClosePragmaAgda.Syntax.Parser.Tokens
SymCloseVirtualBraceAgda.Syntax.Parser.Tokens
SymColonAgda.Syntax.Parser.Tokens
SymDotAgda.Syntax.Parser.Tokens
SymEllipsisAgda.Syntax.Parser.Tokens
SymEqualAgda.Syntax.Parser.Tokens
SymLambdaAgda.Syntax.Parser.Tokens
SymOpenBraceAgda.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
SyntaxAgda.Syntax.Concrete
syntaxOfAgda.Syntax.Fixity