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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - S

S |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base
2 (Data Constructor) | Agda.Mimer.Options
safeButNotBuiltin | Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
safeFlag | Agda.Interaction.Options
SafeFlagEta | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagEta_ | Agda.Interaction.Options.Warnings
SafeFlagInjective | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagInjective_ | Agda.Interaction.Options.Warnings
SafeFlagNoCoverageCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNoCoverageCheck_ | Agda.Interaction.Options.Warnings
SafeFlagNonTerminating | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNonTerminating_ | Agda.Interaction.Options.Warnings
SafeFlagNoPositivityCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNoPositivityCheck_ | Agda.Interaction.Options.Warnings
SafeFlagNoUniverseCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagNoUniverseCheck_ | Agda.Interaction.Options.Warnings
SafeFlagPolarity | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
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.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
SafeFlagTerminating_ | Agda.Interaction.Options.Warnings
SafeFlagWithoutKFlagPrimEraseEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SafeFlagWithoutKFlagPrimEraseEquality_ | Agda.Interaction.Options.Warnings
SafeMode | Agda.Interaction.Options.Lenses
sameCohesion | Agda.Syntax.Common
sameDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
samePolarity | 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
saturateOpaqueBlocks | Agda.TypeChecking.Opacity
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.SplitClause, Agda.TypeChecking.Coverage
sccs | Agda.Utils.Graph.AdjacencyMap.Unidirectional
sccs' | Agda.Utils.Graph.AdjacencyMap.Unidirectional
sChecked | Agda.Interaction.Response.Base, Agda.Interaction.Response
SClause | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
Scope |
1 (Type/Class) | Agda.Syntax.Scope.Base
2 (Data Constructor) | Agda.Syntax.Scope.Base
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.Base, 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
ScopedDeclS | 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
scopeRecords | 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.SplitClause, Agda.TypeChecking.Coverage
scSubst | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
scTarget | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
scTel | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
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.Syntax.Abstract
Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sectIsSection | Agda.Syntax.Notation
sectKind | Agda.Syntax.Notation
sectLevel | Agda.Syntax.Notation
sectNotation | Agda.Syntax.Notation
Self | Agda.Compiler.JS.Syntax
self | Agda.Compiler.JS.Substitution
semi | Agda.Syntax.Common.Pretty
Semigroup | Agda.Utils.Semigroup
SemiRing | Agda.Utils.SemiRing
Semiring |
1 (Type/Class) | Agda.Termination.Semiring
2 (Data Constructor) | Agda.Termination.Semiring
sep |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
SeqArg |
1 (Type/Class) | Agda.Compiler.Treeless.Subst
2 (Data Constructor) | Agda.Compiler.Treeless.Subst
seqP | Agda.Utils.Parser.MemoisedCPS
seqPO | Agda.Utils.PartialOrd
sequenceAFoldable | Agda.TypeChecking.Pretty
sequenceListT | Agda.Utils.ListT
Sequential | Agda.Compiler.ToTreeless
SerialisedRange |
1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Common
2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Common
Serialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Serialize | Agda.Utils.ProfileOptions
Series | Agda.Interaction.JSON
SessionTCState |
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
set | Agda.Utils.Lens
Set1 | Agda.Utils.Set1
setAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
setAnnotation | Agda.Syntax.Common
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
SetBindingSite | Agda.Syntax.Scope.Base
setBindingSite | Agda.Syntax.Scope.Base
setBlockingVarOverlap | Agda.TypeChecking.Coverage.Match
setBuiltinThings | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setCohesion | Agda.Syntax.Common
setCohesionMod | Agda.Syntax.Common
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
setContext | Agda.Syntax.Parser.Monad
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
setHardCompileTimeModeIfErased | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setHardCompileTimeModeIfErased' | 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
setInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setInterface | Agda.Compiler.Common
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
setLock | Agda.Syntax.Common
setMatchableSymbols | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
setMetaGeneralizableArgInfo | 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
setModalPolarity | Agda.Syntax.Common
setModeUnlessInHardCompileTimeMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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.TypeChecking.Monad, Agda.Compiler.Backend
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
setPolarityMod | Agda.Syntax.Common
setPragmaOptions |
1 (Function) | Agda.Interaction.Options
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
setPristineCohesion | Agda.Syntax.Concrete.Attribute
setPristineLock | Agda.Syntax.Concrete.Attribute
setPristinePolarity | Agda.Syntax.Concrete.Attribute
setPristineQuantity | Agda.Syntax.Concrete.Attribute
setPristineRelevance | Agda.Syntax.Concrete.Attribute
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
setRecordConstructor | Agda.Syntax.Scope.Monad
setRelevance | Agda.Syntax.Common
setRelevanceMod | Agda.Syntax.Common
setRunTimeModeUnlessInHardCompileTimeMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
setTacticAttr | Agda.Syntax.Parser.Helpers
setTCLens | Agda.TypeChecking.Monad.Base, 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
setup | Agda.Setup
setupDotEmacs | Agda.Setup.EmacsMode
setupFlag | Agda.Setup.EmacsMode
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.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
SeveralAgdaLibFiles | Agda.Interaction.Library.Base
SeveralConstructors | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ShadowedModule_ | Agda.Interaction.Options.Errors
ShadowingInTelescope |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
ShadowingInTelescope_ | Agda.Interaction.Options.Warnings
ShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shadowLocal | Agda.Syntax.Scope.Base
ShapeIrrelevant | Agda.Syntax.Common
shapeIrrelevant | Agda.Syntax.Common
shapeIrrelevantToIrrelevant | Agda.Syntax.Common
shapeIrrelevantToRelevant | Agda.Syntax.Common
Sharing | Agda.Utils.ProfileOptions
sharing | Agda.Utils.Update
shift | Agda.Compiler.JS.Substitution
shifter | Agda.Compiler.JS.Substitution
shiftFrom | Agda.Compiler.JS.Substitution
ShouldAcceptAtLeastTwoArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeASort_ | Agda.Interaction.Options.Errors
ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeEmpty_ | Agda.Interaction.Options.Errors
ShouldBePath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBePath | Agda.TypeChecking.Telescope
ShouldBePath_ | Agda.Interaction.Options.Errors
ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
shouldBePi | Agda.TypeChecking.Telescope
shouldBePiOrPath | Agda.TypeChecking.Telescope
ShouldBePi_ | Agda.Interaction.Options.Errors
shouldBeProjectible | Agda.TypeChecking.Records
ShouldBeRecordPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordPattern_ | Agda.Interaction.Options.Errors
ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldBeRecordType_ | Agda.Interaction.Options.Errors
shouldBeSort | Agda.TypeChecking.Sort
ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShouldEndInApplicationOfTheDatatype_ | Agda.Interaction.Options.Errors
shouldPostponeInstanceSearch | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.TypeChecking.InstanceArguments, Agda.Compiler.Backend
shouldReduceDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showA | Agda.Syntax.Abstract.Pretty
showATop | Agda.Syntax.Abstract.Pretty
showChar' | Agda.Syntax.Literal
showComputed | Agda.Interaction.BasicOps
showGeneralizedArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showGoals | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop
ShowHead | Agda.TypeChecking.Rules.Decl
showHead | Agda.TypeChecking.Rules.Decl
showIdentitySubstitutions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ShowImplicitArgs | Agda.Interaction.Base
showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
showInfoError | Agda.Interaction.EmacsTop
showIOException | Agda.Utils.IO
ShowIrrelevantArgs | Agda.Interaction.Base
showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
showUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SigCubicalNotErasure | 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
sigInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sigmaCon | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
sigmaFst | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
SigmaKit |
1 (Type/Class) | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
2 (Data Constructor) | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
sigmaName | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
sigmaSnd | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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
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.TypeChecking.Monad, Agda.Compiler.Backend
Simplified | Agda.Interaction.Base
Simplify | Agda.TypeChecking.Reduce
simplify | Agda.TypeChecking.Reduce
simplify1 |
1 (Function) | Agda.TypeChecking.SizedTypes.Syntax
2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver
simplifyBlocked' | Agda.TypeChecking.Reduce
simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints
simplifyTTerm | Agda.Compiler.Treeless.Simplify
simplifyWithHypotheses | Agda.TypeChecking.SizedTypes.WarshallSolver
SingleClosed | Agda.TypeChecking.Level
singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SingleLevel | Agda.TypeChecking.Level
SingleLevel' | Agda.TypeChecking.Level
singleLevelView | Agda.TypeChecking.Level
SinglePass | Agda.Compiler.ToTreeless
SinglePlus | Agda.TypeChecking.Level
Singleton | Agda.Utils.Singleton
singleton |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.VarSet
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.Set1
5 (Function) | Agda.Utils.Bag
6 (Function) | Agda.Utils.BoolSet
7 (Function) | Agda.Utils.IntSet.Infinite
8 (Function) | Agda.Utils.SmallSet
9 (Function) | Agda.Utils.Singleton
10 (Function) | Agda.Utils.Trie
11 (Function) | Agda.Utils.BiMap
12 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
13 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
singletonDT | Agda.TypeChecking.DiscrimTree.Types
SingletonRecords | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
singletonS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SingleVar | Agda.TypeChecking.Free.Lazy
singPlural | Agda.Syntax.Common.Pretty
Size |
1 (Type/Class) | Agda.Termination.SparseMatrix
2 (Data Constructor) | Agda.Termination.SparseMatrix
size |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Bag
4 (Function) | Agda.Utils.BoolSet
5 (Function) | Agda.Utils.Size
6 (Function) | Agda.Termination.SparseMatrix
sizeBuiltins | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeConstraint | Agda.TypeChecking.SizedTypes.Syntax
sizeConstraint | Agda.TypeChecking.SizedTypes.Syntax
sizeContext | Agda.TypeChecking.SizedTypes.Syntax
Sized | Agda.Utils.Size
sizedText | Agda.Syntax.Common.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 | Agda.TypeChecking.SizedTypes.Syntax
sizeExpr | Agda.TypeChecking.SizedTypes.Solve
SizeExpr' | Agda.TypeChecking.SizedTypes.Syntax
sizeHypIds | Agda.TypeChecking.SizedTypes.Syntax
sizeHypotheses | Agda.TypeChecking.SizedTypes.Syntax
SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SizeLtSat | Agda.Interaction.Base
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 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor) | Agda.TypeChecking.SizedTypes
sizeMetaArgs | Agda.TypeChecking.SizedTypes.Syntax
sizeMetaId | Agda.TypeChecking.SizedTypes.Syntax
SizeOfSort |
1 (Type/Class) | Agda.TypeChecking.Substitute
2 (Data Constructor) | Agda.TypeChecking.Substitute
sizeOfSort | Agda.TypeChecking.Substitute
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
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 | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
skip | Agda.Syntax.Parser.LexActions
skipBlock | Agda.Syntax.Parser.Comments
skipIrrelevantAt | Agda.TypeChecking.Rules.LHS.Unify.Types
SkipIrrelevantEquation | Agda.TypeChecking.Rules.LHS.Unify.Types
SleepingConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
slowNormaliseArgs | Agda.TypeChecking.Reduce
slowReduceTerm | Agda.TypeChecking.Reduce
smallest | Agda.TypeChecking.SizedTypes.WarshallSolver
SmallSet |
1 (Type/Class) | Agda.Utils.SmallSet
2 (Data Constructor) | Agda.Utils.SmallSet
SmallSetElement | Agda.Utils.SmallSet
SmallSort | Agda.TypeChecking.Substitute
smashTel | Agda.Syntax.Concrete.Pretty
snd3 | Agda.Utils.Tuple
snoc |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
3 (Function) | Agda.Utils.List2
Solution |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types
solutionAt | Agda.TypeChecking.Rules.LHS.Unify.Types
solutionSide | Agda.TypeChecking.Rules.LHS.Unify.Types
solutionTerm | Agda.TypeChecking.Rules.LHS.Unify.Types
solutionType | Agda.TypeChecking.Rules.LHS.Unify.Types
solutionVar | Agda.TypeChecking.Rules.LHS.Unify.Types
solveAwakeConstraints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveAwakeConstraints' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveAwakeInstanceConstraints | Agda.TypeChecking.InstanceArguments
solveCluster | Agda.TypeChecking.SizedTypes.Solve
solveConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveConstraintTCM | Agda.TypeChecking.Constraints
solveConstraint_ | Agda.TypeChecking.Constraints
SolvedButOpenHoles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SolvedButOpenHoles_ | Agda.Interaction.Options.Errors
solvedMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveEq | Agda.TypeChecking.Rules.LHS.Unify.Types
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.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
solveSomeAwakeConstraintsTCM | Agda.TypeChecking.Constraints
solveVar | Agda.TypeChecking.Rules.LHS.Unify.Types
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
some1 | Agda.Utils.List1
SomeBuiltin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
someBuiltin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SomeGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SomeKindsOfNames | Agda.Syntax.Scope.Base
someKindsOfNames | Agda.Syntax.Scope.Base
SomeWhere | Agda.Syntax.Concrete
SomeWhere_ | Agda.Syntax.Concrete
Sort |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Reflected
5 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
sort |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.TypeChecking.Substitute
Sort' | Agda.Syntax.Internal
sortBy | Agda.Utils.List1
SortCannotDependOnItsIndex | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortCannotDependOnItsIndex_ | Agda.Interaction.Options.Errors
SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortDefs | Agda.Compiler.Common
SortDoesNotAdmitDataDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortDoesNotAdmitDataDefinitions_ | Agda.Interaction.Options.Errors
sorted | Agda.Utils.List
sortFitsIn | Agda.TypeChecking.Sort
SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortInteractionPoints | Agda.Interaction.InteractionTop
SortIntervalUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortK | Agda.TypeChecking.DiscrimTree.Types
SortKit |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortLevelUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortOf | Agda.TypeChecking.Sort
SortOfSplitVarError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortOfSplitVarError_ | Agda.Interaction.Options.Errors
sortOfType | Agda.TypeChecking.Sort
SortOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortOn | Agda.Utils.List1
sortPair | Agda.Utils.Tuple
SortProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortPropOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortRulesOfSymbol | Agda.TypeChecking.Rewriting.Confluence
SortSet | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortSetOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortStrictSet | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortStrictSetOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SortUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sortUniv | Agda.Syntax.Internal
sortWith | Agda.Utils.List1
Source |
1 (Type/Class) | Agda.Interaction.Imports
2 (Data Constructor) | Agda.Interaction.Imports
source |
1 (Function) | Agda.Utils.BiMap
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
SourceFile |
1 (Type/Class) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.Interaction.FindFile, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.Interaction.FindFile, Agda.TypeChecking.Monad, Agda.Compiler.Backend
sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
Space | Agda.Compiler.JS.Pretty
space |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
Span |
1 (Type/Class) | Agda.Syntax.Common.Pretty
2 (Data Constructor) | Agda.Syntax.Common.Pretty
span | Agda.Utils.List1
spanAllowedBeforeModule | Agda.Syntax.Concrete
spanAnnotation | Agda.Syntax.Common.Pretty
spanAntitone |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
spanEnd | Agda.Utils.List
spanJust | Agda.Utils.List
spanLength | Agda.Syntax.Common.Pretty
spanMaybe | Agda.Utils.Maybe
spanStart | Agda.Syntax.Common.Pretty
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.TypeChecking.Monad, Agda.Compiler.Backend
speculateMetas | Agda.TypeChecking.Monad.MetaVars, 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
spLhsDefName | Agda.Syntax.Abstract
spLhsInfo | Agda.Syntax.Abstract
spLhsPats | Agda.Syntax.Abstract
split |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
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.Set1
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.RangeMap
splitBindings | Agda.TypeChecking.Coverage.SplitTree
splitC | Agda.TypeChecking.CompiledClause.Compile
SplitCatchall | Agda.TypeChecking.Coverage.SplitTree
SplitClause | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
splitClauses | Agda.TypeChecking.Coverage.SplitClause, 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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
splitErrorName | Agda.TypeChecking.Errors.Names
splitErrorNameString | Agda.Interaction.Options.Errors
SplitError_ |
1 (Type/Class) | Agda.Interaction.Options.Errors
2 (Data Constructor) | Agda.Interaction.Options.Errors
splitExactlyAt | Agda.Utils.List
splitExcludedLits | Agda.TypeChecking.Coverage.Match
splitImplicitBinderT | Agda.TypeChecking.Implicit
SplitInProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitInProp_ | Agda.Interaction.Options.Errors
splitLast | Agda.TypeChecking.Coverage
splitLazy | Agda.TypeChecking.Coverage.SplitTree
SplitLit | Agda.TypeChecking.Coverage.SplitTree
splitLookup | Agda.Utils.Map1
splitMember | Agda.Utils.Set1
splitOffTrailingWithPatterns | Agda.Syntax.Abstract.Pattern
splitOn | Agda.TypeChecking.CompiledClause.Compile
SplitOnAbstract | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnAbstract_ | Agda.Interaction.Options.Errors
SplitOnCoinductive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnCoinductive_ | Agda.Interaction.Options.Errors
SplitOnFlat | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnIrrelevant_ | Agda.Interaction.Options.Errors
SplitOnNonEtaRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnNonEtaRecord_ | Agda.Interaction.Options.Errors
SplitOnNonVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnNonVariable_ | Agda.Interaction.Options.Errors
SplitOnPartial | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnPartial_ | Agda.Interaction.Options.Errors
SplitOnStrict | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
SplitOnUnchecked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnUnchecked_ | Agda.Interaction.Options.Errors
SplitOnUnusableCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnUnusableCohesion_ | Agda.Interaction.Options.Errors
SplitOnUnusablePolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SplitOnUnusablePolarity_ | Agda.Interaction.Options.Errors
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
splitRoot |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
splitS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
splittableCohesion | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
splittablePolarity | Agda.Syntax.Common
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
srcAttributes | Agda.Interaction.Imports
SrcFile | Agda.Syntax.Position
srcFile | Agda.Syntax.Position
srcFileId | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.Interaction.FindFile, Agda.TypeChecking.Monad, Agda.Compiler.Backend
srcFileOfInterface | Agda.Interaction.Highlighting.HTML.Base
srcFilePath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
srcFileType | Agda.Interaction.Imports
srcFromPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
SSet | Agda.Syntax.Internal
sShowImplicitArguments | Agda.Interaction.Response.Base, Agda.Interaction.Response
sShowIrrelevantArguments | Agda.Interaction.Response.Base, Agda.Interaction.Response
sSizeUniv | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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.TypeChecking.Monad, Agda.Compiler.Backend
Stack | Agda.TypeChecking.CompiledClause.Match
StaleMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StaleMeta_ | Agda.Interaction.Options.Errors
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
stateTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stateTCLensM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Base, Agda.Interaction.Response
2 (Data Constructor) | Agda.Interaction.Response.Base, 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
stBuiltinModuleIds | 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
stCopiedNames | 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
StdErr | Agda.TypeChecking.Unquote
StdIn | Agda.TypeChecking.Unquote
stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StdOut | Agda.TypeChecking.Unquote
stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stealConstraintsTCM | Agda.TypeChecking.Constraints
sTextC | Agda.TypeChecking.Serialise.Base
sTextD | Agda.TypeChecking.Serialise.Base
sTextE | Agda.TypeChecking.Serialise.Base
stFileDict | Agda.TypeChecking.Monad.Base, 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
stFreshOpaqueId | 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
stImportedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedModulesTransitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stImportedPartialDefs | 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
stInstanceHack | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInstanceTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stInstantiateBlocking | 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
stLibCache | 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
stLocalPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stLocalUserWarnings | 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
stModuleToSourceId | 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
stNameCopies | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stOpenMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeCachedAgdaLibFile | Agda.Interaction.Library.Base
storeCachedProjectConfig | Agda.Interaction.Library.Base
storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
storeDisambiguatedConstructor | Agda.Interaction.Highlighting.Generate
storeDisambiguatedProjection | 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
stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentSession | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistentTopLevelModuleNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPersistLoadedFileCache | 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
stPostForeignCode | 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
stPostFreshOpaqueId | 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
stPostInstanceHack | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostInstantiateBlocking | 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
stPostLocalPartialDefs | 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
stPostOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostOpenMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostPendingInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostponeInstanceSearch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostPostponeInstanceSearch | 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
stPostSolvedMetaStore | 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
stPostTemporaryInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPostUsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreCopiedNames | 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
stPreImportedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedModulesTransitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreImportedPartialDefs | 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
stPreLibCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreModuleToSourceId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPreNameCopies | 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
stPreWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stPrimitiveLibDir | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Strengthen | Agda.Syntax.Internal, Agda.TypeChecking.Substitute
strengthen | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
strengthenS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
strengthenS' | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
stRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Strict |
1 (Type/Class) | Agda.Utils.Maybe.Strict
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
strictCurry | Agda.Utils.TypeLevel
StrictCurrying | Agda.Utils.TypeLevel
strictCurrys | Agda.Utils.TypeLevel
StrictlyPositive | Agda.Syntax.Common
Strictness | Agda.Utils.Haskell.Syntax
StrictPair | Agda.Utils.TypeLevel
StrictPos | Agda.TypeChecking.Positivity.Occurrence
StrictProducts | Agda.Utils.TypeLevel
StrictSplit | Agda.TypeChecking.Coverage.SplitTree
strictUncurry | Agda.Utils.TypeLevel
strictUncurrys | Agda.Utils.TypeLevel
String |
1 (Data Constructor) | Agda.Interaction.JSON
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
3 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
4 (Data Constructor) | Agda.Compiler.JS.Syntax
String1 | Agda.Utils.List1
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
stringToArgName | Agda.Syntax.Common
stringToAttribute | Agda.Syntax.Concrete.Attribute
stringToRawName | Agda.Syntax.Common
stripAgdaExtension | Agda.Interaction.FindFile
stripAnyOfExtensions | Agda.Utils.FileName
stripArgLeft | Agda.TypeChecking.Rules.LHS.Unify.Types
stripArgRight | Agda.TypeChecking.Rules.LHS.Unify.Types
stripAt | Agda.TypeChecking.Rules.LHS.Unify.Types
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
StripSizeSuc | Agda.TypeChecking.Rules.LHS.Unify.Types
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.TypeChecking.Monad, Agda.Compiler.Backend
stSessionBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSessionBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stSessionFileDict | 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
stSolvedMetaStore | 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
stTemporaryInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stTopLevelModuleNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
StuckOn | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stuckOn | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
stUsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
stWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Style |
1 (Type/Class) | Agda.Syntax.Common.Pretty
2 (Data Constructor) | Agda.Syntax.Common.Pretty
style | Agda.Syntax.Common.Pretty
Sub | Agda.TypeChecking.Rewriting.NonLinMatch
subLevel | Agda.TypeChecking.Level
Subscript | Agda.Utils.Suffix
Subst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subst |
1 (Function) | Agda.Compiler.JS.Substitution
2 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
3 (Function) | Agda.TypeChecking.SizedTypes.Syntax
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
substShift | Agda.Compiler.JS.Substitution
substUnder | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
SubstWith | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
subtract | Agda.Utils.VarSet
subtypingForSizeLt | Agda.TypeChecking.MetaVars
subVar | Agda.TypeChecking.Free.Lazy
Suc | Agda.Utils.IndexedList
Succ | Agda.Utils.Size
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
suffixesSatisfying | Agda.Utils.List
suffixNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
suffixToLevel | Agda.TypeChecking.Rules.Application
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
superscript | Agda.TypeChecking.Pretty
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 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
3 (Type/Class) | Agda.Syntax.Parser.Tokens
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
syntacticEqualityFuelRemains | Agda.TypeChecking.SyntacticEquality
Syntax | Agda.Syntax.Concrete
SyntaxBindingLambda | Agda.Syntax.Concrete
SyntaxError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
syntaxError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
SyntaxError_ | Agda.Interaction.Options.Errors
syntaxOf | Agda.Syntax.Notation
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
szSortSize | Agda.TypeChecking.Substitute
szSortUniv | Agda.TypeChecking.Substitute