Agda-2.2.6: 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
SemiRingAgda.Utils.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
sEqsAgda.Auto.Convert
Set 
1 (Data Constructor)Agda.Syntax.Concrete
2 (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
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
setOptionsFromPragmasAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setParsePosAgda.Syntax.Parser.Monad
setPolarityAgda.TypeChecking.Monad.Signature, 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
setTraceAgda.TypeChecking.Monad.Trace, 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
shouldReifyInteractionPointsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showAAgda.Syntax.Abstract.Pretty
showAsOptimizedConstructorAgda.Compiler.Agate.OptimizedPrinter
ShowAsOptimizedKindAgda.Compiler.Agate.OptimizedPrinter
showAsOptimizedKindAgda.Compiler.Agate.OptimizedPrinter
ShowAsOptimizedTermAgda.Compiler.Agate.OptimizedPrinter
showAsOptimizedTermAgda.Compiler.Agate.OptimizedPrinter
ShowAsOptimizedTypeAgda.Compiler.Agate.OptimizedPrinter
showAsOptimizedTypeAgda.Compiler.Agate.OptimizedPrinter
showAsUntypedConstructorAgda.Compiler.Agate.UntypedPrinter
ShowAsUntypedTermAgda.Compiler.Agate.UntypedPrinter
showAsUntypedTermAgda.Compiler.Agate.UntypedPrinter
showBehaviourAgda.Termination.CallGraph
showChar'Agda.Syntax.Concrete.Pretty
showClauseAgda.Compiler.Agate.Common
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
showNumIIdAgda.Interaction.GhciTop
showOptimizedClauseAgda.Compiler.Agate.OptimizedPrinter
showOptimizedDefinitionsAgda.Compiler.Agate.OptimizedPrinter
showOptimizedLiteralAgda.Compiler.Agate.Common
showPatAgda.TypeChecking.With
showScopeAgda.Interaction.CommandLine.CommandLine
showStatusAgda.Interaction.GhciTop
showString'Agda.Syntax.Concrete.Pretty
showTypeDeclarationAgda.Compiler.Agate.OptimizedPrinter
showTypeDeclarationsAgda.Compiler.Agate.OptimizedPrinter
showTypeParameterAgda.Compiler.Agate.OptimizedPrinter
showUntypedAppAgda.Compiler.Agate.UntypedPrinter
showUntypedClauseAgda.Compiler.Agate.UntypedPrinter
showUntypedDefinitionAgda.Compiler.Agate.UntypedPrinter
showUntypedLiteralAgda.Compiler.Agate.Common
showValueDefinitionAgda.Compiler.Agate.OptimizedPrinter
showValueDefinitionsAgda.Compiler.Agate.OptimizedPrinter
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
SiblingCallAgda.Utils.Trace
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
Size 
1 (Type/Class)Agda.Termination.Matrix
2 (Data Constructor)Agda.Termination.Matrix
size 
1 (Function)Agda.Utils.Size
2 (Function)Agda.Termination.Matrix
3 (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
sizeInvariantAgda.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
smallestPosAgda.Interaction.Highlighting.Precise
Smart 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
sMetasAgda.Auto.Convert
SolutionAgda.Utils.Warshall
solveAgda.Utils.Warshall
solveConstraintAgda.TypeChecking.Constraints
solveConstraintsAgda.TypeChecking.Constraints
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
SortLevelAgda.Auto.Syntax
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
SplitClauseAgda.TypeChecking.Coverage
splitClauseAgda.TypeChecking.Coverage
splitClauseWithAbsAgda.TypeChecking.Coverage
SplitError 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Type/Class)Agda.TypeChecking.Coverage
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
splitTypeAgda.Compiler.Agate.Common
squareAgda.Termination.Matrix
srcFileAgda.Syntax.Position, Agda.Interaction.GhciTop
SResAgda.Auto.NarrowingSearch
sShowImplicitArgumentsAgda.Interaction.GhciTop
sSucAgda.Syntax.Internal
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
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
stTraceAgda.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.Typecheck
SubConstraints 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
SubstAgda.TypeChecking.Substitute
substAgda.TypeChecking.Substitute
SubstitutionAgda.TypeChecking.Rules.LHS.Problem
substsAgda.TypeChecking.Substitute
substUnderAgda.TypeChecking.Substitute
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