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

- 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.Auto.Convert
2 (Data Constructor) | Agda.Auto.Convert
SafeFlagNoTerminationCheck | 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
Same | Agda.Compiler.Epic.Injection
sameVars | Agda.TypeChecking.Conversion
sample | Agda.Utils.QuickCheck
sample' | Agda.Utils.QuickCheck
satisfy | Agda.Utils.ReadP
sccomcount | Agda.Auto.NarrowingSearch
sccs | Agda.Utils.Graph
sccs' | Agda.Utils.Graph
scflip | Agda.Auto.NarrowingSearch
sChecked | Agda.Interaction.Response
SClause | 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
scopeCurrent | Agda.Syntax.Scope.Base
scopeDatatypeModule | Agda.Syntax.Scope.Base
ScopedDecl | Agda.Syntax.Abstract
ScopedExpr | Agda.Syntax.Abstract
scopeImports | Agda.Syntax.Scope.Base
ScopeInfo |
1 (Type/Class) | Agda.Syntax.Scope.Base
2 (Data Constructor) | Agda.Syntax.Scope.Base
scopeLocals | Agda.Syntax.Scope.Base
scopeLookup | Agda.Syntax.Scope.Base
scopeLookup' | Agda.Syntax.Scope.Base
ScopeM | Agda.Syntax.Scope.Monad
scopeModules | Agda.Syntax.Scope.Base
scopeName | Agda.Syntax.Scope.Base
scopeNameSpace | Agda.Syntax.Scope.Base
scopeNameSpaces | Agda.Syntax.Scope.Base
scopeParents | Agda.Syntax.Scope.Base
scopePrecedence | Agda.Syntax.Scope.Base
scPats | Agda.TypeChecking.Coverage
scPerm | 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
secFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
Self | Agda.Compiler.JS.Syntax
self | Agda.Compiler.JS.Substitution
semi | Agda.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
semiringInvariant | Agda.Termination.Semiring
sep |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
sepBy | Agda.Utils.ReadP
sepBy1 | Agda.Utils.ReadP
seqc | Agda.Auto.NarrowingSearch
seqctx | Agda.Auto.CaseSplit
sEqs | Agda.Auto.Convert
Set |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
set | Agda.Syntax.Internal
set0 | Agda.Syntax.Internal
setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setBuiltinThings | Agda.TypeChecking.Monad.Builtin
setCommandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setCommandLineOptions' | Agda.Interaction.InteractionTop
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
setExtLambdaTele | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setFreqs | Agda.TypeChecking.Test.Generators
setImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInput | Agda.Syntax.Parser.LookAhead
setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInterface | Agda.Compiler.MAlonzo.Misc
setLastPos | Agda.Syntax.Parser.Monad
setLexInput | Agda.Syntax.Parser.Alex
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
SetN | Agda.Syntax.Concrete
setNameSpace | Agda.Syntax.Scope.Base
SetOmegaNotValidType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setParsePos | Agda.Syntax.Parser.Monad
setPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setPragmaOptions | 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
setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setScopeAccess | Agda.Syntax.Scope.Base
setSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTag | Agda.Compiler.Epic.Injection
setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
several | Agda.Interaction.Highlighting.Precise
severalC | Agda.Interaction.Highlighting.Precise
ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShapeView | Agda.TypeChecking.Rules.LHS.Unify
shapeView | Agda.TypeChecking.Rules.LHS.Unify
shapeViewHH | Agda.TypeChecking.Rules.LHS.Unify
Shared | Agda.Syntax.Internal
shared | Agda.Syntax.Internal
sharedType | Agda.Syntax.Internal
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
shouldEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
shouldReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showA | Agda.Syntax.Abstract.Pretty
showATop | Agda.Syntax.Abstract.Pretty
showChar' | Agda.Syntax.Concrete.Pretty
showComparison | Agda.Interaction.BasicOps
showConstraints | Agda.Interaction.CommandLine.CommandLine
showContext | Agda.Interaction.CommandLine.CommandLine
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.CommandLine
showModuleContents | Agda.Interaction.InteractionTop
showPat | Agda.TypeChecking.With
showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
showScope | Agda.Interaction.CommandLine.CommandLine
showString' | Agda.Syntax.Concrete.Pretty
shrink | Agda.Utils.QuickCheck
Shrink2 |
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
ShrinkC | Agda.TypeChecking.Test.Generators
shrinkC | Agda.TypeChecking.Test.Generators
Shrinking |
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
shrinking | Agda.Utils.QuickCheck
shrinkInit | Agda.Utils.QuickCheck
shrinkIntegral | Agda.Utils.QuickCheck
shrinkNothing | Agda.Utils.QuickCheck
shrinkRealFrac | Agda.Utils.QuickCheck
ShrinkState | Agda.Utils.QuickCheck
shrinkState | Agda.Utils.QuickCheck
Sidecondition | Agda.Auto.NarrowingSearch
Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigMName | Agda.Compiler.MAlonzo.Misc
Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints
singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
singleton |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.Trie
4 (Function) | Agda.Utils.Graph
5 (Function) | Agda.Interaction.Highlighting.Precise
singletonC | Agda.Interaction.Highlighting.Precise
SingletonRecords | Agda.TypeChecking.MetaVars
singletonS | Agda.TypeChecking.Substitute
Size |
1 (Type/Class) | Agda.Termination.Matrix
2 (Data Constructor) | Agda.Termination.Matrix
3 (Type/Class) | Agda.Termination.SparseMatrix
4 (Data Constructor) | Agda.Termination.SparseMatrix
size |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Termination.Matrix
3 (Function) | Agda.Utils.Size
4 (Function) | Agda.Termination.SparseMatrix
5 (Function) | Agda.Termination.Lexicographic
SizeConst | Agda.Utils.Warshall
SizeConstraint | Agda.TypeChecking.SizedTypes
Sized | Agda.Utils.Size
sized | Agda.Utils.QuickCheck
SizedList |
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
sizedText | Agda.Utils.Pretty
SizeExpr |
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.SizedTypes
sizeExpr | Agda.TypeChecking.SizedTypes
SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeInvariant |
1 (Function) | Agda.Termination.Matrix
2 (Function) | Agda.Termination.SparseMatrix
sizeMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeMaxView | Agda.TypeChecking.SizedTypes
SizeMeta | Agda.TypeChecking.SizedTypes
sizePolarity | Agda.TypeChecking.Polarity
sizeRigid | Agda.Utils.Warshall
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
sizeType | 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.ReadP
skipMany1 | Agda.Utils.ReadP
skipSpaces | Agda.Utils.ReadP
sLub | Agda.TypeChecking.Substitute
sMainMeta | Agda.Auto.Convert
smallestPos | Agda.Interaction.Highlighting.Precise
smallestPosC | Agda.Interaction.Highlighting.Precise
Smart |
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
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 | Agda.Utils.Warshall
solve |
1 (Function) | Agda.Utils.Warshall
2 (Function) | Agda.Compiler.Epic.Injection
solveAwakeConstraints | Agda.TypeChecking.Constraints
solveAwakeConstraints' | Agda.TypeChecking.Constraints
solveConstraint | Agda.TypeChecking.Constraints
solveConstraint_ | Agda.TypeChecking.Constraints
solveIrrelevantMetas | Agda.TypeChecking.InstanceArguments
solveMetaIfIrrelevant | Agda.TypeChecking.InstanceArguments
solveSizeConstraints | Agda.TypeChecking.SizedTypes
solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
SomeWhere | Agda.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
sort | Agda.Syntax.Internal
SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sorted | Agda.Utils.List
sortFreq | Agda.TypeChecking.Test.Generators
SortFreqs |
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
sortFreqs | Agda.TypeChecking.Test.Generators
SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortInteractionPoints | Agda.Interaction.InteractionTop
sortOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
SortSh | Agda.TypeChecking.Rules.LHS.Unify
sortTm | Agda.TypeChecking.Substitute
source | Agda.Termination.CallGraph
SourceToModule | Agda.Interaction.FindFile
sourceToModule | Agda.Interaction.FindFile
space | Agda.Utils.Pretty
SpineLHS |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Abstract
splashScreen | Agda.Interaction.CommandLine.CommandLine
spLhsDefName | Agda.Syntax.Abstract
spLhsInfo | Agda.Syntax.Abstract
spLhsPats | Agda.Syntax.Abstract
spLhsWithPats | Agda.Syntax.Abstract
Split | Agda.TypeChecking.Rules.LHS.Problem
split | Agda.TypeChecking.Coverage
split' | Agda.TypeChecking.Coverage
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
splitClauseWithAbs | Agda.TypeChecking.Coverage
splitDbIndexToLevel | Agda.TypeChecking.Coverage
SplitError |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Type/Class) | Agda.TypeChecking.Coverage
splitLast | Agda.TypeChecking.Coverage
splitOn | Agda.TypeChecking.CompiledClause.Compile
SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SplitPanic | Agda.TypeChecking.Rules.LHS.Problem
splitPerm | Agda.TypeChecking.Telescope
SplitProblem | Agda.TypeChecking.Rules.LHS.Problem
splitProblem | Agda.TypeChecking.Rules.LHS.Split
splitS | Agda.TypeChecking.Substitute
splitStrategy | Agda.TypeChecking.Coverage
SplitTel |
1 (Type/Class) | Agda.TypeChecking.Telescope
2 (Data Constructor) | Agda.TypeChecking.Telescope
splitTelescope | Agda.TypeChecking.Telescope
SplittingDone | Agda.TypeChecking.Coverage.SplitTree
splitTrailingImplicits | Agda.TypeChecking.Rules.Def
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 |
1 (Function) | Agda.Termination.Matrix
2 (Function) | Agda.Termination.SparseMatrix
srcFile | Agda.Syntax.Position
SRes | Agda.Auto.NarrowingSearch
sShowImplicitArguments | Agda.Interaction.Response
sSuc | Agda.Syntax.Internal
Stack | Agda.TypeChecking.CompiledClause.Match
standardOptions_ | Agda.Interaction.Options
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
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
stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stdArgs | Agda.Utils.QuickCheck
stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
step | Agda.Compiler.Epic.Erasure
stExtLambdaTele | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPersistent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPragmaOptions | Agda.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
StrictPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
String |
1 (Data Constructor) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
string | Agda.Utils.ReadP
stringChr | Agda.Compiler.JS.Parser
stringLit | Agda.Compiler.JS.Parser
stringParts | Agda.Syntax.Notation
stringStr | Agda.Compiler.JS.Parser
stripDontCare | Agda.Syntax.Internal
stripNoNames | Agda.Syntax.Scope.Monad
stripWithClausePatterns | Agda.TypeChecking.With
strongly | Agda.TypeChecking.MetaVars.Occurs
StronglyRigid |
1 (Data Constructor) | Agda.TypeChecking.Free
2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs
StronglyRigidOccurrence | Agda.TypeChecking.Rules.LHS.Unify
stronglyRigidVars | Agda.TypeChecking.Free
stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTermErrs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Style |
1 (Type/Class) | Agda.Utils.Pretty
2 (Data Constructor) | Agda.Utils.Pretty
style | Agda.Utils.Pretty
Sub |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Unify
sub | Agda.Auto.Syntax
SubConstraints |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
subi | Agda.Auto.Syntax
Subscript | Agda.Utils.Suffix
Subst | Agda.TypeChecking.Substitute
subst |
1 (Function) | Agda.Compiler.JS.Substitution
2 (Function) | Agda.Compiler.Epic.AuxAST
3 (Function) | 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
substForDot | Agda.Compiler.Epic.Injection
SubstHH | Agda.TypeChecking.Rules.LHS.Unify
substHH | Agda.TypeChecking.Rules.LHS.Unify
substituter | Agda.Compiler.JS.Substitution
Substitution |
1 (Type/Class) | Agda.TypeChecking.Substitute
2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
substLetBinding | Agda.Syntax.Abstract
substLit | Agda.Compiler.Epic.FromAgda
substPattern | Agda.Syntax.Abstract
substs | Agda.Compiler.Epic.AuxAST
substTerm | Agda.Compiler.Epic.FromAgda
substTypedBinding | Agda.Syntax.Abstract
substTypedBindings | Agda.Syntax.Abstract
substUnder | Agda.TypeChecking.Substitute
substUnderHH | Agda.TypeChecking.Rules.LHS.Unify
subsvars | Agda.Auto.SearchControl
subtract | Agda.Utils.VarSet
Success | Agda.Utils.QuickCheck
suchThat | Agda.Utils.QuickCheck
suchThatMaybe | Agda.Utils.QuickCheck
sucName | Agda.TypeChecking.Level
Suffix |
1 (Type/Class) | Agda.Utils.List
2 (Type/Class) | Agda.Utils.Suffix
suffixView | Agda.Utils.Suffix
supremum | Agda.Termination.CallGraph
SymArrow | Agda.Syntax.Parser.Tokens
SymAs | Agda.Syntax.Parser.Tokens
SymBar | Agda.Syntax.Parser.Tokens
Symbol |
1 (Data Constructor) | Agda.Interaction.Highlighting.Precise
2 (Type/Class) | Agda.Syntax.Parser.Tokens
symbol | Agda.Syntax.Parser.LexActions
SymCloseBrace | 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
SymEqual | Agda.Syntax.Parser.Tokens
SymLambda | Agda.Syntax.Parser.Tokens
SymOpenBrace | 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
Syntax | Agda.Syntax.Concrete
SyntaxBindingLambda | Agda.Syntax.Concrete
syntaxOf | Agda.Syntax.Fixity