Agda-2.6.0.1: 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 (Data Constructor) | Agda.Auto.Options
2 (Type/Class) | Agda.TypeChecking.Serialise.Base
3 (Type/Class) | Agda.Auto.Convert
4 (Data Constructor) | Agda.Auto.Convert
safeFlag | Agda.Interaction.Options
SafeFlagNonTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNonTerminating_ | Agda.Interaction.Options.Warnings
SafeFlagNoPositivityCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNoPositivityCheck_ | Agda.Interaction.Options.Warnings
SafeFlagNoUniverseCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagNoUniverseCheck_ | Agda.Interaction.Options.Warnings
SafeFlagPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagPolarity_ | Agda.Interaction.Options.Warnings
SafeFlagPostulate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagPostulate_ | Agda.Interaction.Options.Warnings
SafeFlagPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagPragma_ | Agda.Interaction.Options.Warnings
SafeFlagTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagTerminating_ | Agda.Interaction.Options.Warnings
SafeFlagWithoutKFlagPrimEraseEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagWithoutKFlagPrimEraseEquality_ | Agda.Interaction.Options.Warnings
safeInTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeMode | Agda.Interaction.Options.Lenses
safePermute | Agda.Utils.Permutation
sameDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sameHiding | Agda.Syntax.Common
sameRoot |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
sameVars | Agda.TypeChecking.Conversion
sanityCheckPragma | Agda.Compiler.MAlonzo.Pragmas
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' |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad
satisfy | Agda.Utils.Parser.ReadP
satNoPlaceholder | Agda.Syntax.Concrete.Operators.Parser
sayWhen | Agda.TypeChecking.Errors
SBool | Agda.Utils.TypeLits
sccDAG | Agda.Utils.Graph.AdjacencyMap.Unidirectional
sccDAG' | Agda.Utils.Graph.AdjacencyMap.Unidirectional
scCheckpoints | Agda.TypeChecking.Coverage
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
sConsts | Agda.Auto.Convert
Scope |
1 (Type/Class) | Agda.Syntax.Scope.Base
2 (Data Constructor) | Agda.Syntax.Scope.Base
3 (Type/Class) | Agda.Utils.Warshall
ScopeCheck | Agda.Interaction.Imports
ScopeCheckDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
scopeCheckImport | Agda.Interaction.Imports
scopeCheckingSuffices | Agda.Compiler.Backend
ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
scopeFixities | Agda.Syntax.Scope.Base
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
scopePolarities | Agda.Syntax.Scope.Base
scopePrecedence | Agda.Syntax.Scope.Base
scopeVarsToBind | 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, Agda.Compiler.Backend
Section |
1 (Data Constructor) | Agda.Syntax.Abstract
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SectionApp |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sectIsSection | Agda.Syntax.Fixity
sectKind | Agda.Syntax.Fixity
sectLevel | Agda.Syntax.Fixity
sectNotation | Agda.Syntax.Fixity
seenUIds | Agda.Auto.Syntax
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
seqP | Agda.Utils.Parser.MemoisedCPS
seqPO | Agda.Utils.PartialOrd
sEqs | Agda.Auto.Convert
SerialisedRange |
1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Common
2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Common
Serialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Set |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
set | Agda.Utils.Lens
setAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
setArgInfo | Agda.Syntax.Common
setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setAttribute | Agda.Syntax.Concrete.Attribute
setAttributes | Agda.Syntax.Concrete.Attribute
setBenchmarking | Agda.Utils.Benchmark
setBlockingVarOverlap | Agda.TypeChecking.Coverage.Match
setBuiltinThings | Agda.TypeChecking.Monad.Builtin
setCommandLineOptions |
1 (Function) | Agda.Interaction.Options.Lenses
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCommandLineOptions' | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCommandLineOpts | Agda.Interaction.InteractionTop
setCompiledArgUse | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCompiledClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setConName | Agda.Syntax.Internal
setContextPrecedence | Agda.Syntax.Scope.Monad
setCurrentModule | Agda.Syntax.Scope.Monad
setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setDebugging | Agda.TypeChecking.SizedTypes.Utils
setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setDefault | Agda.Utils.WithDefault
setErasedConArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setFoldl | Agda.TypeChecking.SizedTypes.WarshallSolver
setFreeVariables | Agda.Syntax.Common
setFreeVariablesArgInfo | Agda.Syntax.Common
setFunctionFlag | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setHiding | Agda.Syntax.Common
setHidingArgInfo | Agda.Syntax.Common
setImportedName | Agda.Syntax.Common
setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setIncludePaths | Agda.Interaction.Options.Lenses
setInput | Agda.Syntax.Parser.LookAhead
setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
setLibraryPaths | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setLocalVars | Agda.Syntax.Scope.Monad
setMetaArgInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaNameSuggestion | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaOccursCheck | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setModality | Agda.Syntax.Common
setModalityArgInfo | Agda.Syntax.Common
setModuleCheckpoint | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMutual | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMutualBlockInfo | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SetN | Agda.Syntax.Concrete
setNamedArg | Agda.Syntax.Common
setNamedScope | Agda.Syntax.Scope.Monad
setNameOf | Agda.Syntax.Common
setNameSpace | Agda.Syntax.Scope.Base
setNotInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setOrigin | Agda.Syntax.Common
setOriginArgInfo | Agda.Syntax.Common
setParsePos | Agda.Syntax.Parser.Monad
setPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setPersistentVerbosity | Agda.Interaction.Options.Lenses
setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setPragmaOptions |
1 (Function) | Agda.Interaction.Options.Lenses
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setPrevToken | Agda.Syntax.Parser.Monad
setPristineAttribute | Agda.Syntax.Concrete.Attribute
setPristineAttributes | Agda.Syntax.Concrete.Attribute
setPristineQuantity | Agda.Syntax.Concrete.Attribute
setPristineRelevance | Agda.Syntax.Concrete.Attribute
setPtr | Agda.Utils.Pointer
setQuantity | Agda.Syntax.Common
setQuantityMod | Agda.Syntax.Common
SetRange |
1 (Type/Class) | Agda.Syntax.Position
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setRange | Agda.Syntax.Position
setRelevance | Agda.Syntax.Common
setRelevanceMod | Agda.Syntax.Common
SetS | Agda.Syntax.Reflected
setSafeMode | Agda.Interaction.Options.Lenses
setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setScopeAccess | Agda.Syntax.Scope.Base
setScopeLocals | Agda.Syntax.Scope.Base
setSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setSplitTree | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SetToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver
setToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver
setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setTreeless | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setUsability | Agda.Termination.Order
setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setVarsToBind | Agda.Syntax.Scope.Base
setVerbosity | Agda.Interaction.Options.Lenses
setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
several | Agda.Interaction.Highlighting.Precise
severalC | Agda.Interaction.Highlighting.Precise
SFalse | Agda.Utils.TypeLits
sgListT | Agda.Utils.ListT
sgMListT | Agda.Utils.ListT
SgTel | Agda.Syntax.Internal
sgTel | Agda.Syntax.Internal
ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shadowLocal | Agda.Syntax.Scope.Base
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, Agda.Compiler.Backend
ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBePath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBeSort | Agda.TypeChecking.CheckInternal
ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldTryFastReduce | Agda.TypeChecking.Reduce
showA | Agda.Syntax.Abstract.Pretty
showATop | Agda.Syntax.Abstract.Pretty
showChar' | Agda.Syntax.Literal
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, Agda.Compiler.Backend
showIndex | Agda.Utils.String
showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
showScope | Agda.Interaction.CommandLine
showString' | Agda.Syntax.Literal
showThousandSep | Agda.Utils.String
Sidecondition | Agda.Auto.NarrowingSearch
siFileType | Agda.Interaction.Imports
Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigError | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigError | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigmaCon | Agda.TypeChecking.Primitive
sigmaFst | Agda.TypeChecking.Primitive
SigmaKit |
1 (Type/Class) | Agda.TypeChecking.Primitive
2 (Data Constructor) | Agda.TypeChecking.Primitive
sigmaName | Agda.TypeChecking.Primitive
sigmaSnd | Agda.TypeChecking.Primitive
sigMName | Agda.Compiler.Common
Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigUnknown | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
siModule | Agda.Interaction.Imports
siModuleName | Agda.Interaction.Imports
Simplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
Singleton | Agda.Utils.Singleton
singleton |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.BiMap
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Utils.IntSet.Infinite
6 (Function) | Agda.Utils.Singleton
7 (Function) | Agda.Utils.Trie
8 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
9 (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
siSource | Agda.Interaction.Imports
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
sizeAndBoundVars | Agda.Auto.CaseSplit
sizeBuiltins | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin
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
sizedTypesOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
SizeLtSat | Agda.Interaction.BasicOps
sizeMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeMaxView | Agda.TypeChecking.SizedTypes
SizeMaxView' | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
SizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeSucName | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeThing | Agda.Utils.Size
sizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeType_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeUniv | Agda.Syntax.Internal
sizeUniv | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeVar | Agda.Utils.Warshall
SizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewComparableWithMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewOffset | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewPred | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sizeViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Skip |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Compiler.Backend
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, Agda.Compiler.Backend
slowNormaliseArgs | Agda.TypeChecking.Reduce
slowReduceTerm | Agda.TypeChecking.Reduce
sMainMeta | Agda.Auto.Convert
smallest | Agda.TypeChecking.SizedTypes.WarshallSolver
smallestPos | Agda.Interaction.Highlighting.Precise
smallestPosC | Agda.Interaction.Highlighting.Precise
smashTel | Agda.Syntax.Concrete.Pretty
sMetas | Agda.Auto.Convert
snd3 | Agda.Utils.Tuple
snoc | Agda.Utils.List
Sol | Agda.Auto.CaseSplit
Solution |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class) | Agda.Utils.Warshall
Solutions | Agda.Auto.Auto
solve | Agda.Utils.Warshall
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, Agda.Compiler.Backend
solveGraph | Agda.TypeChecking.SizedTypes.WarshallSolver
solveGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver
solveInstantiatedGoals | Agda.Interaction.InteractionTop
solveSizeConstraints | Agda.TypeChecking.SizedTypes.Solve
solveSizeConstraints_ | Agda.TypeChecking.SizedTypes.Solve
solveSomeAwakeConstraints | Agda.TypeChecking.Constraints
solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solvingProblems | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Some |
1 (Type/Class) | Agda.Utils.IndexedList
2 (Data Constructor) | Agda.Utils.IndexedList
SomeGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SomeWarnings | Agda.Interaction.Imports
SomeWhere | Agda.Syntax.Concrete
Sort |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Reflected
5 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
6 (Type/Class) | Agda.Syntax.Internal
7 (Data Constructor) | Agda.Syntax.Internal
sort | Agda.Syntax.Internal
SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortDefs | Agda.Compiler.Common
sorted | Agda.Utils.List
sortFitsIn | Agda.TypeChecking.Sort
SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortInteractionPoints | Agda.Interaction.InteractionTop
source | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
SourceInfo |
1 (Type/Class) | Agda.Interaction.Imports
2 (Data Constructor) | Agda.Interaction.Imports
sourceInfo | Agda.Interaction.Imports
sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
SourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
space | Agda.Utils.Pretty
spanAllowedBeforeModule | Agda.Syntax.Concrete
spanEnd | Agda.Utils.List
spanJust | Agda.Utils.List
SpecialCharacters |
1 (Type/Class) | Agda.Syntax.Concrete.Pretty
2 (Data Constructor) | Agda.Syntax.Concrete.Pretty
specialCharacters | Agda.Syntax.Concrete.Pretty
Specified | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpeculateAbort | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpeculateCommit | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpeculateResult | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
speculateTCState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
speculateTCState_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SpineClause | Agda.Syntax.Abstract
SpineLHS |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Abstract
spineToLhs | Agda.Syntax.Abstract.Pattern
spineToLhsCore | Agda.Syntax.Abstract.Pattern
splashScreen | Agda.Interaction.CommandLine
spLhsDefName | Agda.Syntax.Abstract
spLhsInfo | Agda.Syntax.Abstract
spLhsPats | Agda.Syntax.Abstract
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
SplitCatchall | Agda.TypeChecking.Coverage.SplitTree
SplitClause | Agda.TypeChecking.Coverage
splitClauses | Agda.TypeChecking.Coverage
splitClauseWithAbsurd | Agda.TypeChecking.Coverage
splitCommas | Agda.Interaction.Library.Parse
SplitCon | Agda.TypeChecking.Coverage.SplitTree
SplitError |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
splitExactlyAt | Agda.Utils.List
splitExcludedLits | Agda.TypeChecking.Coverage.Match
splitLast | Agda.TypeChecking.Coverage
SplitLit | Agda.TypeChecking.Coverage.SplitTree
splitOffTrailingWithPatterns | Agda.Syntax.Abstract.Pattern
splitOn | Agda.TypeChecking.CompiledClause.Compile
splitOnDots | Agda.Syntax.Parser.Parser
SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnNonVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitPattern | Agda.TypeChecking.Coverage.Match
SplitPatVar |
1 (Type/Class) | Agda.TypeChecking.Coverage.Match
2 (Data Constructor) | Agda.TypeChecking.Coverage.Match
splitPatVarIndex | Agda.TypeChecking.Coverage.Match
splitPatVarName | Agda.TypeChecking.Coverage.Match
splitPerm | Agda.TypeChecking.Telescope
splitResult | Agda.TypeChecking.Coverage
splitS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SplitTag | Agda.TypeChecking.Coverage.SplitTree
SplitTel |
1 (Type/Class) | Agda.TypeChecking.Telescope
2 (Data Constructor) | Agda.TypeChecking.Telescope
splitTelescope | Agda.TypeChecking.Telescope
splitTelescopeAt | 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
SSSMismatch | Agda.Utils.List
SSSResult | Agda.Utils.List
SSSStrip | Agda.Utils.List
St |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base
2 (Data Constructor) | Agda.TypeChecking.Serialise.Base
stAccumStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Stack | Agda.TypeChecking.CompiledClause.Match
standardOptions | Agda.Interaction.Options
standardOptions_ | Agda.Interaction.Options
stAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
starP | Agda.Utils.Parser.MemoisedCPS
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, Agda.Compiler.Backend
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, Agda.Compiler.Backend
stBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Stmt | Agda.Utils.Haskell.Syntax
stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeDisambiguatedName | Agda.Interaction.Highlighting.Generate
stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostTCWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrePatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrePatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
Strict | Agda.Utils.Haskell.Syntax
Strictness | Agda.Utils.Haskell.Syntax
StrictPos | Agda.TypeChecking.Positivity.Occurrence
String |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
string | Agda.Utils.Parser.ReadP
string2HelpTopic | Agda.Interaction.Options.Help
string2WarningName | Agda.Interaction.Options.Warnings
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
stringTCErr | Agda.TypeChecking.Errors
stringToArgName | Agda.Syntax.Internal
stringToAttribute | Agda.Syntax.Concrete.Attribute
stringToRawName | Agda.Syntax.Common
stripDontCare | Agda.Syntax.Internal
stripNoNames | Agda.Syntax.Scope.Monad
stripPrefixBy | Agda.Utils.List
stripReversedSuffix | Agda.Utils.List
stripRTS | Agda.Interaction.Options
stripSuffix | 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
3 (Data Constructor) | Agda.TypeChecking.Free.Old
4 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs
stronglyRigidVars |
1 (Function) | Agda.TypeChecking.Free
2 (Function) | Agda.TypeChecking.Free.Old
StrPart | Agda.TypeChecking.Unquote
StrSufSt | Agda.Utils.List
STrue | Agda.Utils.TypeLits
stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTCWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StuckOn | Agda.Syntax.Internal
stuckOn | Agda.Syntax.Internal
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Style |
1 (Data Constructor) | Agda.Utils.Pretty
2 (Type/Class) | Agda.Utils.Pretty
style | Agda.Utils.Pretty
Sub |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch
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
subscriptAllowed | 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.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subst' | Agda.Compiler.JS.Substitution
substBody | Agda.TypeChecking.CompiledClause.Compile
SubstCand | Agda.TypeChecking.MetaVars
SubstExpr | Agda.Syntax.Abstract
substExpr | Agda.Syntax.Abstract
Substitute | Agda.TypeChecking.SizedTypes.Syntax
substituter | Agda.Compiler.JS.Substitution
Substitution |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Internal, Agda.TypeChecking.Substitute
Substitution' | Agda.Syntax.Internal, Agda.TypeChecking.Substitute
substPattern | Agda.Syntax.Abstract.Pattern
substPattern' | Agda.Syntax.Abstract.Pattern
substUnder | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SubstWithOrigin | Agda.TypeChecking.DisplayForm
substWithOrigin | Agda.TypeChecking.DisplayForm
subsvars | Agda.Auto.SearchControl
subtract | Agda.Utils.VarSet
subtypingForSizeLt | Agda.TypeChecking.MetaVars
subVar | Agda.TypeChecking.Free.Lazy
Suc | Agda.Utils.IndexedList
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
System |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
systemClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
systemTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend