Agda-2.6.2.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 (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
SafeFlagEta | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagEta_ | Agda.Interaction.Options.Warnings
SafeFlagInjective | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagInjective_ | Agda.Interaction.Options.Warnings
SafeFlagNoCoverageCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNoCoverageCheck_ | Agda.Interaction.Options.Warnings
SafeFlagNonTerminating | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNonTerminating_ | Agda.Interaction.Options.Warnings
SafeFlagNoPositivityCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNoPositivityCheck_ | Agda.Interaction.Options.Warnings
SafeFlagNoUniverseCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagNoUniverseCheck_ | Agda.Interaction.Options.Warnings
SafeFlagPolarity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagPolarity_ | Agda.Interaction.Options.Warnings
SafeFlagPostulate | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagPostulate_ | Agda.Interaction.Options.Warnings
SafeFlagPragma | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagPragma_ | Agda.Interaction.Options.Warnings
SafeFlagTerminating | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagTerminating_ | Agda.Interaction.Options.Warnings
SafeFlagWithoutKFlagPrimEraseEquality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SafeFlagWithoutKFlagPrimEraseEquality_ | Agda.Interaction.Options.Warnings
SafeMode | Agda.Interaction.Options.Lenses
safePermute | Agda.Utils.Permutation
sameCohesion | Agda.Syntax.Common
sameDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sameErased | Agda.Syntax.Common
sameFile | Agda.Utils.FileName
sameHiding | Agda.Syntax.Common
sameKind | Agda.Syntax.Concrete.Definitions.Types
sameModality | Agda.Syntax.Common
sameName | Agda.Syntax.Common
sameQuantity | Agda.Syntax.Common
sameRelevance | 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
satNoPlaceholder | Agda.Syntax.Concrete.Operators.Parser
sayWhen | Agda.TypeChecking.Pretty.Call
sayWhere | Agda.TypeChecking.Pretty.Call
SBool | Agda.Utils.TypeLits
scanl | Agda.Utils.List1
scanl1 | Agda.Utils.List1
scanr | Agda.Utils.List1
scanr1 | Agda.Utils.List1
scatterMP | Agda.Utils.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
scopeCheckImport | Agda.Interaction.Imports
scopeCheckingSuffices | Agda.Compiler.Backend
ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
scopeFixitiesAndPolarities | 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
scopeWarning | Agda.Syntax.Scope.Monad
scopeWarning' | Agda.Syntax.Scope.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
Section |
1 (Data Constructor) | Agda.Syntax.Abstract
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SectionApp |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Sections | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sectIsSection | Agda.Syntax.Notation
sectKind | Agda.Syntax.Notation
sectLevel | Agda.Syntax.Notation
sectNotation | Agda.Syntax.Notation
seenUIds | Agda.Auto.Syntax
Self | Agda.Compiler.JS.Syntax
self | Agda.Compiler.JS.Substitution
semi | Agda.Utils.Pretty
Semigroup | Agda.Utils.Semigroup, Agda.TypeChecking.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
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
sequenceListT | Agda.Utils.ListT
SerialisedRange |
1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Common
2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Common
Serialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Series | Agda.Interaction.JSON
Set | Agda.Auto.Syntax
set | Agda.Utils.Lens
setAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
setAnnotation | Agda.Syntax.Common
setArgInfo | Agda.Syntax.Common
setArgOccurrences | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setAttribute | Agda.Syntax.Concrete.Attribute
setAttributes | Agda.Syntax.Concrete.Attribute
setBenchmarking | Agda.Utils.Benchmark
SetBindingSite | Agda.Syntax.Scope.Base
setBindingSite | Agda.Syntax.Scope.Base
setBlockingVarOverlap | Agda.TypeChecking.Coverage.Match
setBuiltinThings | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
setCohesion | Agda.Syntax.Common
setCohesionMod | Agda.Syntax.Common
setCommandLineOptions |
1 (Function) | Agda.Interaction.Options.Lenses
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setCommandLineOptions' | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setCommandLineOpts | Agda.Interaction.InteractionTop
setCompiledArgUse | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setCompiledClauses | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setConName | Agda.Syntax.Internal
setContext | Agda.Syntax.Parser.Monad
setContextPrecedence | Agda.Syntax.Scope.Monad
setCurrentModule | Agda.Syntax.Scope.Monad
setCurrentRange | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
setDebugging | Agda.TypeChecking.SizedTypes.Utils
setDecodedModules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
setDefault | Agda.Utils.WithDefault
setErasedConArgs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setEtaEquality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setFoldl | Agda.TypeChecking.SizedTypes.WarshallSolver
setFreeVariables | Agda.Syntax.Common
setFreeVariablesArgInfo | Agda.Syntax.Common
setFunctionFlag | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setHiding | Agda.Syntax.Common
setHidingArgInfo | Agda.Syntax.Common
setImportedName | Agda.Syntax.Common
setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setIncludePaths | Agda.Interaction.Options.Lenses
setInput | Agda.Syntax.Parser.LookAhead
setInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setInterface | Agda.Compiler.Common
setIntervalFile | Agda.Syntax.Position
setLastPos | Agda.Syntax.Parser.Monad
setLexInput | Agda.Syntax.Parser.Alex
setLibraryIncludes | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setLibraryPaths | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setLocalVars | Agda.Syntax.Scope.Monad
setLock | Agda.Syntax.Common
setMatchableSymbols | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setMetaGeneralizableArgInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setMetaNameSuggestion | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setMetaOccursCheck | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setModality | Agda.Syntax.Common
setModalityArgInfo | Agda.Syntax.Common
setModuleCheckpoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setMutual | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setMutualBlock | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
setMutualBlockInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
setNamedArg | Agda.Syntax.Common
setNamedScope | Agda.Syntax.Scope.Monad
setNameOf | Agda.Syntax.Common
setNameSpace | Agda.Syntax.Scope.Base
setNameSuffix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setNotInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setOrigin | Agda.Syntax.Common
setOriginArgInfo | Agda.Syntax.Common
setParsePos | Agda.Syntax.Parser.Monad
setPatternSyns | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setPersistentVerbosity | Agda.Interaction.Options.Lenses
setPolarity | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setPragmaOptions |
1 (Function) | Agda.Interaction.Options.Lenses
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setPrevToken | Agda.Syntax.Parser.Monad
setPristineAttribute | Agda.Syntax.Concrete.Attribute
setPristineAttributes | Agda.Syntax.Concrete.Attribute
setPristineCohesion | Agda.Syntax.Concrete.Attribute
setPristineLock | 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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
setScopeAccess | Agda.Syntax.Scope.Base
setScopeLocals | Agda.Syntax.Scope.Base
setSignature | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setSplitTree | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setTCLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setTerminates | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
SetToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver
setToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver
setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
setTreeless | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
setUsability | Agda.Termination.Order
setValueMetaName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
setVarsToBind | Agda.Syntax.Scope.Base
setVerbosity | Agda.Interaction.Options.Lenses
setVisitedModules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
several | Agda.Utils.RangeMap, 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.Compiler.Backend, Agda.TypeChecking.Monad
ShadowingInTelescope |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
ShadowingInTelescope_ | Agda.Interaction.Options.Warnings
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.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBePath | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeRecordPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
shouldBeSort | Agda.TypeChecking.Sort, Agda.TypeChecking.CheckInternal
ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
shouldPostponeInstanceSearch | Agda.TypeChecking.InstanceArguments
shouldReduceDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
shouldTryFastReduce | Agda.TypeChecking.Reduce
showA | Agda.Syntax.Abstract.Pretty
showATop | Agda.Syntax.Abstract.Pretty
showChar' | Agda.Syntax.Literal
showComputed | Agda.Interaction.BasicOps
showGoals | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop
ShowHead | Agda.TypeChecking.Rules.Decl
showHead | Agda.TypeChecking.Rules.Decl
showIdentitySubstitutions | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ShowImplicitArgs | Agda.Interaction.Base
showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
showInfoError | Agda.Interaction.EmacsTop
ShowIrrelevantArgs | Agda.Interaction.Base
showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
showModuleContents | Agda.Interaction.InteractionTop
showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
showText | Agda.Syntax.Literal
showThousandSep | Agda.Utils.String
Sidecondition | Agda.Auto.NarrowingSearch
Sig | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SigAbstract | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SigError | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sigError | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
sigmaCon | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
sigmaFst | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
SigmaKit |
1 (Type/Class) | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
2 (Data Constructor) | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
sigmaName | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
sigmaSnd | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
Signature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sigSections | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SigUnknown | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
simpleBinaryOperator | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
simpleHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
simpleName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Simplification | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Simplified | Agda.Interaction.Base
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
SingleClosed | Agda.TypeChecking.Level
singleConstructorType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
SingleLevel | Agda.TypeChecking.Level
SingleLevel' | Agda.TypeChecking.Level
singleLevelView | Agda.TypeChecking.Level
SinglePlus | Agda.TypeChecking.Level
Singleton | Agda.Utils.Singleton
singleton |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.VarSet
3 (Function) | Agda.Utils.Bag
4 (Function) | Agda.Utils.IntSet.Infinite
5 (Function) | Agda.Utils.Singleton
6 (Function) | Agda.Utils.SmallSet
7 (Function) | Agda.Utils.Trie
8 (Function) | Agda.Utils.BiMap
9 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
10 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
SingletonRecords | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
singletonS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SingleVar | Agda.TypeChecking.Free.Lazy
singPlural | Agda.Utils.Pretty
Size |
1 (Type/Class) | Agda.Termination.SparseMatrix
2 (Data Constructor) | Agda.Termination.SparseMatrix
size |
1 (Function) | Agda.Utils.Bag
2 (Function) | Agda.Utils.Size
3 (Function) | Agda.Termination.SparseMatrix
sizeAndBoundVars | Agda.Auto.CaseSplit
sizeBuiltins | Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, 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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeLtSat | Agda.Interaction.Base
sizeMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeMaxView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeMaxView | Agda.TypeChecking.SizedTypes
SizeMaxView' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
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
sizeRigid | Agda.Utils.Warshall
sizeSort | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeSuc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeSuc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeSucName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeSuc_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeThing | Agda.Utils.Size
sizeType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeType_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeUniv | Agda.Syntax.Internal
sizeUniv | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeVar | Agda.Utils.Warshall
SizeView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
SizeViewComparable | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewComparable | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewComparableWithMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewOffset | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewPred | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
sizeViewSuc_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
Skip |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Compiler.Backend
skip | Agda.Syntax.Parser.LexActions
skipBlock | Agda.Syntax.Parser.Comments
SleepingConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
slowNormaliseArgs | Agda.TypeChecking.Reduce
slowReduceTerm | Agda.TypeChecking.Reduce
sMainMeta | Agda.Auto.Convert
smallest | Agda.TypeChecking.SizedTypes.WarshallSolver
SmallSet | Agda.Utils.SmallSet
smashTel | Agda.Syntax.Concrete.Pretty
sMetas | Agda.Auto.Convert
snd3 | Agda.Utils.Tuple
snoc |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
solveConstraintTCM | Agda.TypeChecking.Constraints
solveConstraint_ | Agda.TypeChecking.Constraints
SolvedButOpenHoles | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
solveSomeAwakeConstraintsTCM | Agda.TypeChecking.Constraints
solvingProblem | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
solvingProblems | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
Some |
1 (Type/Class) | Agda.Utils.IndexedList
2 (Data Constructor) | Agda.Utils.IndexedList
some1 | Agda.Utils.List1
SomeGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SomeKindsOfNames | Agda.Syntax.Scope.Base
someKindsOfNames | Agda.Syntax.Scope.Base
SomeWhere | Agda.Syntax.Concrete
Sort |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Auto.Syntax
3 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
4 (Type/Class) | Agda.Syntax.Internal
5 (Data Constructor) | Agda.Syntax.Internal
6 (Type/Class) | Agda.Syntax.Reflected
7 (Data Constructor) | Agda.Syntax.Reflected
sort |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.TypeChecking.Substitute
Sort' | Agda.Syntax.Internal
sortBy | Agda.Utils.List1
SortCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sortDefs | Agda.Compiler.Common
sorted | Agda.Utils.List
sortFitsIn | Agda.TypeChecking.Sort
SortHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sortInteractionPoints | Agda.Interaction.InteractionTop
SortKit |
1 (Type/Class) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
2 (Data Constructor) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
sortKit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
sortOf | Agda.TypeChecking.Sort
SortOfSplitVarError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sortOfType | Agda.TypeChecking.Sort
sortRulesOfSymbol | Agda.TypeChecking.Rewriting.Confluence
sortWith | Agda.Utils.List1
Source |
1 (Type/Class) | Agda.Interaction.Imports
2 (Data Constructor) | Agda.Interaction.Imports
source | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
SourceFile |
1 (Type/Class) | Agda.Interaction.FindFile
2 (Data Constructor) | Agda.Interaction.FindFile
sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
SourceToModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
sourceToModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Space | Agda.Compiler.JS.Pretty
space |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
span | Agda.Utils.List1
spanAllowedBeforeModule | Agda.Syntax.Concrete
spanEnd | Agda.Utils.List
spanJust | Agda.Utils.List
SpecialCharacters |
1 (Type/Class) | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
2 (Data Constructor) | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
specialCharactersForGlyphs | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
Specified | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SpeculateAbort | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SpeculateCommit | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
speculateMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
SpeculateResult | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
speculateTCState | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
speculateTCState_ | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
spLhsDefName | Agda.Syntax.Abstract
spLhsInfo | Agda.Syntax.Abstract
spLhsPats | Agda.Syntax.Abstract
splitApplyElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
splitArg | Agda.TypeChecking.Coverage.SplitTree
SplitAt | Agda.TypeChecking.Coverage.SplitTree
splitAt |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.RangeMap
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
splitEllipsis | Agda.Syntax.Concrete.Pattern
SplitError |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
splitExactlyAt | Agda.Utils.List
splitExcludedLits | Agda.TypeChecking.Coverage.Match
splitLast | Agda.TypeChecking.Coverage
splitLazy | Agda.TypeChecking.Coverage.SplitTree
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.Compiler.Backend, Agda.TypeChecking.Monad
SplitOnNonEtaRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SplitOnNonVariable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
SplitOnUnusableCohesion | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
splittableCohesion | Agda.TypeChecking.Irrelevance
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
Squash | Agda.Syntax.Common
src | Agda.TypeChecking.SizedTypes.WarshallSolver
SrcFile | Agda.Syntax.Position
srcFile | Agda.Syntax.Position
srcFilePath | Agda.Interaction.FindFile
srcFileType | Agda.Interaction.Imports
SrcFun | Agda.Utils.CallStack
SrcLoc |
1 (Data Constructor) | Agda.Utils.CallStack
2 (Type/Class) | Agda.Utils.CallStack
SrcLocCol | Agda.Utils.CallStack
srcLocEndCol | Agda.Utils.CallStack
srcLocEndLine | Agda.Utils.CallStack
SrcLocFile | Agda.Utils.CallStack
srcLocFile | Agda.Utils.CallStack
SrcLocLine | Agda.Utils.CallStack
SrcLocModule | Agda.Utils.CallStack
srcLocModule | Agda.Utils.CallStack
SrcLocPackage | Agda.Utils.CallStack
srcLocPackage | Agda.Utils.CallStack
srcLocStartCol | Agda.Utils.CallStack
srcLocStartLine | Agda.Utils.CallStack
srcModule | Agda.Interaction.Imports
srcModuleName | Agda.Interaction.Imports
srcNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
srcOrigin | Agda.Interaction.Imports
srcProjectLibs | Agda.Interaction.Imports
srcText | Agda.Interaction.Imports
SRes | Agda.Auto.NarrowingSearch
SSet | Agda.Syntax.Internal
sShowImplicitArguments | Agda.Interaction.Response
sShowIrrelevantArguments | Agda.Interaction.Response
sSizeUniv | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
ssort | Agda.TypeChecking.Substitute
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.Compiler.Backend, Agda.TypeChecking.Monad
Stack | Agda.TypeChecking.CompiledClause.Match
stAgdaLibFiles | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
standardOptions | Agda.Interaction.Options
standardOptions_ | Agda.Interaction.Options
stAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
starP | Agda.Utils.Parser.MemoisedCPS
StarSemiRing | Agda.Utils.SemiRing
startPos | Agda.Syntax.Position
startPos' | Agda.Syntax.Position
stateTCLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stateTCLensM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StaticPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Statistics | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
stBackends | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stBenchmark | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StdErr | Agda.TypeChecking.Unquote
StdIn | Agda.TypeChecking.Unquote
stDirty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StdOut | Agda.TypeChecking.Unquote
stealConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
stealConstraintsTCM | Agda.TypeChecking.Constraints
sTextC | Agda.TypeChecking.Serialise.Base
sTextD | Agda.TypeChecking.Serialise.Base
sTextE | Agda.TypeChecking.Serialise.Base
stForeignCode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshInt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshNameId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedPartialDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportedUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImports | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInstantiateBlocking | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLocalPartialDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stMetaStore | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Stmt | Agda.Utils.Haskell.Syntax
stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
storeCachedAgdaLibFile | Agda.Interaction.Library.Base
storeCachedProjectConfig | Agda.Interaction.Library.Base
storeDecodedModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
storeDisambiguatedConstructor | Agda.Interaction.Highlighting.Generate
storeDisambiguatedProjection | Agda.Interaction.Highlighting.Generate
stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistBackends | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistentState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPersistLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostCurrentModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostDirty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshInt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshNameId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostInstantiateBlocking | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostLocalPartialDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostMetaStore | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostponeInstanceSearch | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostPostponeInstanceSearch | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostScopeState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostShadowingNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostStatistics | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostTCWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPostUsedNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreAgdaLibFiles | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreForeignCode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedPartialDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImportedUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreImports | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreModuleToSource | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPrePatternSynImports | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPrePatternSyns | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPrePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreProjectConfigs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreScopeState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreTokens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreVisitedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stPreWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stProjectConfigs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
StrictSplit | Agda.TypeChecking.Coverage.SplitTree
String |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
4 (Data Constructor) | Agda.Interaction.JSON
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.Common
stringToAttribute | Agda.Syntax.Concrete.Attribute
stringToRawName | Agda.Syntax.Common
stripConstraintPids | Agda.Interaction.BasicOps
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
strongly | Agda.TypeChecking.MetaVars.Occurs
StronglyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
stronglyRigidVars | Agda.TypeChecking.Free
StrPart | Agda.TypeChecking.Unquote
StrSufSt | Agda.Utils.List
STrue | Agda.Utils.TypeLits
stScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stShadowingNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stStatistics | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stTCWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stTokens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
StuckOn | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stuckOn | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stUsedNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
stWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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
SubstArg | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute, Agda.TypeChecking.Substitute
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
SubstWith | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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
3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
suffixView | Agda.Utils.Suffix
Suggest | Agda.Syntax.Internal
Suggestion |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
suggestName | Agda.Syntax.Internal
suggests | Agda.Syntax.Internal
SumEncoding | Agda.Interaction.JSON
sumEncoding | Agda.Interaction.JSON
supremum | Agda.Termination.Order
supSize | Agda.Termination.SparseMatrix
swap | Agda.Utils.Tuple
swap01 | Agda.TypeChecking.Abstract
swapEither | Agda.Utils.Either
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
SymEmptyIdiomBracket | 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.Notation
System |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
systemClauses | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
systemTel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad