Agda-2.2.6: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ!$+./<=>|-
Index (S)
S
1 (Type/Class)
2 (Data Constructor)
sameVars
sample
sample'
satisfy
sccomcount
scflip
sChecked
SClause
sConsts
Scope
1 (Type/Class)
2 (Data Constructor)
3 (Type/Class)
ScopeCheckDeclaration
ScopeCheckDefinition
ScopeCheckExpr
scopeCheckImport
ScopeCheckLHS
scopeCurrent
ScopedDecl
ScopedDef
ScopedExpr
scopeImported
scopeImports
ScopeInfo
1 (Type/Class)
2 (Data Constructor)
scopeLocals
scopeLookup
ScopeM
scopeModules
scopeName
scopeNameSpace
scopeParents
scopePrecedence
scopePrivate
scopePublic
scPats
scPerm
scsub1
scsub2
scSubst
scTel
sCurMeta
secFreeVars
secondPart
secTelescope
Section
1 (Data Constructor)
2 (Type/Class)
3 (Data Constructor)
Sections
semi
SemiRing
Semiring
1 (Type/Class)
2 (Data Constructor)
semiringInvariant
sep
1 (Function)
2 (Function)
sepBy
sepBy1
seqc
sEqs
Set
1 (Data Constructor)
2 (Data Constructor)
set
set0
setArgOccurrences
setBuiltinThings
setCommandLineOptions
1 (Function)
2 (Function)
setContextPrecedence
setCurrentModule
setCurrentRange
setDecodedModules
setFreqs
setImportedSignature
setInput
setInputFile
setInterface
setLastPos
setLexInput
setLocalVars
setMutualBlock
SetN
setOptionsFromPragma
setOptionsFromPragmas
setParsePos
setPolarity
setPrevToken
SetRange
1 (Type/Class)
2 (Data Constructor)
setRange
setScope
setScopeAccess
setShowImplicitArguments
setSignature
setTopLevelModule
setTrace
setVisitedModules
several
ShadowedModule
ShouldBeApplicationOf
ShouldBeAppliedToTheDatatypeParameters
ShouldBeASort
ShouldBeEmpty
ShouldBePi
ShouldBeRecordType
ShouldEndInApplicationOfTheDatatype
shouldReifyInteractionPoints
showA
showAsOptimizedConstructor
ShowAsOptimizedKind
showAsOptimizedKind
ShowAsOptimizedTerm
showAsOptimizedTerm
ShowAsOptimizedType
showAsOptimizedType
showAsUntypedConstructor
ShowAsUntypedTerm
showAsUntypedTerm
showBehaviour
showChar'
showClause
showComparison
showConstraints
showContext
showHighlightingInfo
showImplicitArgs
showImplicitArguments
showIndex
showMetas
showNumIId
showOptimizedClause
showOptimizedDefinitions
showOptimizedLiteral
showPat
showScope
showStatus
showString'
showTypeDeclaration
showTypeDeclarations
showTypeParameter
showUntypedApp
showUntypedClause
showUntypedDefinition
showUntypedLiteral
showValueDefinition
showValueDefinitions
shrink
Shrink2
1 (Data Constructor)
2 (Type/Class)
ShrinkC
shrinkC
Shrinking
1 (Data Constructor)
2 (Type/Class)
shrinking
shrinkInit
shrinkIntegral
shrinkNothing
shrinkRealFrac
ShrinkState
shrinkState
SiblingCall
Sig
sigDefinitions
sigMName
Signature
sigSections
singleConstructorType
singleton
1 (Function)
2 (Function)
3 (Function)
Size
1 (Type/Class)
2 (Data Constructor)
size
1 (Function)
2 (Function)
3 (Function)
SizeConst
SizeConstraint
Sized
sized
SizedList
1 (Type/Class)
2 (Data Constructor)
SizeExpr
1 (Type/Class)
2 (Type/Class)
sizeExpr
SizeInf
sizeInvariant
SizeMeta
sizePolarity
sizeRigid
SizeSuc
sizeSuc
sizeType
SizeVar
SizeView
sizeView
Skip
skipBlock
skipMany
skipMany1
skipSpaces
sLub
smallestPos
Smart
1 (Data Constructor)
2 (Type/Class)
sMetas
Solution
solve
solveConstraint
solveConstraints
solveSizeConstraints
SomeWhere
Sort
1 (Data Constructor)
2 (Type/Class)
3 (Type/Class)
4 (Data Constructor)
sort
SortCmp
sortFreq
SortFreqs
1 (Type/Class)
2 (Data Constructor)
sortFreqs
SortHead
sortInteractionPoints
SortLevel
sortOfConst
source
SourceToModule
sourceToModule
space
splashScreen
Split
split
split'
SplitClause
splitClause
splitClauseWithAbs
SplitError
1 (Type/Class)
2 (Type/Class)
SplitPanic
splitPerm
SplitProblem
splitProblem
SplitTel
1 (Type/Class)
2 (Data Constructor)
splitTelescope
splitType
square
srcFile
SRes
sShowImplicitArguments
sSuc
standardOptions_
startPos
State
1 (Type/Class)
2 (Data Constructor)
Statistics
Status
1 (Type/Class)
2 (Data Constructor)
status
stBuiltinThings
stConstraints
stCurrentModule
stdArgs
stDecodedModules
stFreshThings
stHaskellImports
stImportedBuiltins
stImportedModules
stImports
stInteractionPoints
stLocalBuiltins
stMetaStore
stModuleToSource
stMutualBlocks
store
storeDecodedModule
stPersistentOptions
stPragmaOptions
Str
1 (Type/Class)
2 (Data Constructor)
3 (Type/Class)
4 (Data Constructor)
Strict
strict
String
string
stripImplicits
stripNoNames
stripWithClausePatterns
stScope
stSignature
stStatistics
stTrace
stVisitedModules
Style
1 (Type/Class)
2 (Data Constructor)
style
Sub
1 (Data Constructor)
2 (Type/Class)
sub
SubConstraints
1 (Type/Class)
2 (Data Constructor)
Subst
subst
Substitution
substs
substUnder
Suc
Success
suchThat
suchThatMaybe
sucName
Suffix
1 (Type/Class)
2 (Type/Class)
suffixView
supremum
SymArrow
SymAs
SymBar
Symbol
1 (Type/Class)
2 (Data Constructor)
symbol
SymCloseBrace
SymCloseParen
SymClosePragma
SymCloseVirtualBrace
SymColon
SymDot
SymEllipsis
SymEqual
SymLambda
SymOpenBrace
SymOpenParen
SymOpenPragma
SymOpenVirtualBrace
SymQuestionMark
SymSemi
SymUnderscore
SymVirtualSemi
sync