| 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 |
| 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.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.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| 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 |
| 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 |
| saturateOpaqueBlocks | Agda.TypeChecking.Opacity |
| 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, Agda.TypeChecking.Coverage.SplitClause |
| 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, Agda.TypeChecking.Coverage.SplitClause |
| 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 |
| 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 |
| 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, Agda.TypeChecking.Coverage.SplitClause |
| scsub1 | Agda.Auto.NarrowingSearch |
| scsub2 | Agda.Auto.NarrowingSearch |
| scSubst | Agda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause |
| scTarget | Agda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause |
| scTel | Agda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause |
| 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.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.Syntax.Common.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.Syntax.Common.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 |
| Serialize | Agda.Utils.ProfileOptions |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| setCommandLineOptions' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| 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 |
| setHardCompileTimeModeIfErased | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| setHardCompileTimeModeIfErased' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| setHiding | Agda.Syntax.Common |
| setHidingArgInfo | Agda.Syntax.Common |
| setImportedName | Agda.Syntax.Common |
| setIncludeDirs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| setIncludePaths | Agda.Interaction.Options.Lenses |
| setInput | Agda.Syntax.Parser.LookAhead |
| setInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| setInteractionOutputCallback | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| setInterface | Agda.Compiler.Common |
| setIntervalFile | Agda.Syntax.Position |
| setLastPos | Agda.Syntax.Parser.Monad |
| setLexInput | Agda.Syntax.Parser.Alex |
| setLibraryIncludes | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| setLibraryPaths | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| setLocalVars | Agda.Syntax.Scope.Monad |
| setLock | Agda.Syntax.Common |
| setMatchableSymbols | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| 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 |
| setModeUnlessInHardCompileTimeMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| setOrigin | Agda.Syntax.Common |
| setOriginArgInfo | Agda.Syntax.Common |
| setParsePos | Agda.Syntax.Parser.Monad |
| setPatternSyns | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| 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 |
| setRunTimeModeUnlessInHardCompileTimeMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| SetS | Agda.Syntax.Reflected |
| setSafeMode | Agda.Interaction.Options.Lenses |
| setScope | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| setScopeAccess | Agda.Syntax.Scope.Base |
| setScopeLocals | Agda.Syntax.Scope.Base |
| setSignature | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| setSplitTree | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| setTCLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| 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 |
| SeveralConstructors | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| ShadowingInTelescope_ | Agda.Interaction.Options.Warnings |
| shadowLocal | Agda.Syntax.Scope.Base |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| shouldBePath | Agda.TypeChecking.Telescope |
| ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| shouldBePi | Agda.TypeChecking.Telescope |
| shouldBePiOrPath | Agda.TypeChecking.Telescope |
| shouldBeProjectible | Agda.TypeChecking.Records |
| 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 |
| ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| shouldPostponeInstanceSearch | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.InstanceArguments |
| shouldReduceDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| showA | Agda.Syntax.Abstract.Pretty |
| showATop | Agda.Syntax.Abstract.Pretty |
| showChar' | Agda.Syntax.Literal |
| showComputed | Agda.Interaction.BasicOps |
| showGeneralizedArguments | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| showGoals | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop |
| ShowHead | Agda.TypeChecking.Rules.Decl |
| showHead | Agda.TypeChecking.Rules.Decl |
| showIdentitySubstitutions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| ShowImplicitArgs | Agda.Interaction.Base |
| showImplicitArguments | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| showInfoError | Agda.Interaction.EmacsTop |
| ShowIrrelevantArgs | Agda.Interaction.Base |
| showIrrelevantArguments | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options |
| 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 |
| 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 |
| SigCubicalNotErasure | 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 |
| 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.BoolSet |
| 4 (Function) | Agda.Utils.Bag |
| 5 (Function) | Agda.Utils.IntSet.Infinite |
| 6 (Function) | Agda.Utils.SmallSet |
| 7 (Function) | Agda.Utils.Singleton |
| 8 (Function) | Agda.Utils.Trie |
| 9 (Function) | Agda.Utils.BiMap |
| 10 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 11 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| 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.Syntax.Common.Pretty |
| Size | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| size | |
| 1 (Function) | Agda.Utils.BoolSet |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.Size |
| 4 (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.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.Compiler.Backend, Agda.TypeChecking.Monad |
| SizeExpr | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 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 |
| SizeOfSort | |
| 1 (Type/Class) | Agda.TypeChecking.Substitute |
| 2 (Data Constructor) | Agda.TypeChecking.Substitute |
| sizeOfSort | Agda.TypeChecking.Substitute |
| 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 |
| skipIrrelevantAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
| SkipIrrelevantEquation | Agda.TypeChecking.Rules.LHS.Unify.Types |
| 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 |
| SmallSetElement | Agda.Utils.SmallSet |
| SmallSort | Agda.TypeChecking.Substitute |
| 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.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 3 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 4 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types |
| solutionAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
| Solutions | Agda.Auto.Auto |
| 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 |
| solve | Agda.Utils.Warshall |
| solveAwakeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| solveAwakeConstraints' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| solveAwakeInstanceConstraints | Agda.TypeChecking.InstanceArguments |
| 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 |
| solvedMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| solveSomeAwakeConstraintsTCM | Agda.TypeChecking.Constraints |
| solveVar | Agda.TypeChecking.Rules.LHS.Unify.Types |
| 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 |
| SomeBuiltin | Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| someBuiltin | Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| 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 (Type/Class) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Type/Class) | Agda.Syntax.Reflected |
| 6 (Data Constructor) | Agda.Syntax.Reflected |
| 7 (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.Compiler.Backend, Agda.TypeChecking.Monad |
| SortCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| sortDefs | Agda.Compiler.Common |
| SortDoesNotAdmitDataDefinitions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| sorted | Agda.Utils.List |
| sortFitsIn | Agda.TypeChecking.Sort |
| SortHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| sortInteractionPoints | Agda.Interaction.InteractionTop |
| SortIntervalUniv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| SortLevelUniv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| sortOf | Agda.TypeChecking.Sort |
| SortOfSplitVarError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| sortOfType | Agda.TypeChecking.Sort |
| SortOmega | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SortProp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SortPropOmega | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| sortRulesOfSymbol | Agda.TypeChecking.Rewriting.Confluence |
| SortSet | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SortSetOmega | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SortStrictSet | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SortStrictSetOmega | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SortUniv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Interaction.FindFile |
| 2 (Data Constructor) | Agda.Interaction.FindFile |
| 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 (Data Constructor) | Agda.Syntax.Common.Pretty |
| 2 (Type/Class) | Agda.Syntax.Common.Pretty |
| span | Agda.Utils.List1 |
| spanAllowedBeforeModule | Agda.Syntax.Concrete |
| spanAnnotation | Agda.Syntax.Common.Pretty |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| SpeculateAbort | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| SpeculateCommit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| speculateMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| SpeculateResult | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| speculateTCState | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| speculateTCState_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.State |
| 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, Agda.TypeChecking.Coverage.SplitClause |
| splitClauses | Agda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause |
| 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 |
| SplitInProp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| splitLast | Agda.TypeChecking.Coverage |
| splitLazy | Agda.TypeChecking.Coverage.SplitTree |
| SplitLit | Agda.TypeChecking.Coverage.SplitTree |
| splitOffTrailingWithPatterns | Agda.Syntax.Abstract.Pattern |
| splitOn | Agda.TypeChecking.CompiledClause.Compile |
| SplitOnAbstract | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| splitOnDots | Agda.Syntax.Parser.Parser |
| SplitOnFlat | Agda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
| 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 |
| SplitOnPartial | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| SplitOnStrict | Agda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
| SplitOnUnchecked | 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Modality |
| 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 |
| 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 |
| stCopiedNames | 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 |
| stFreshOpaqueId | 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 |
| stImportedMetaStore | 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 |
| 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 |
| stNameCopies | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| stOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| stOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| stOpenMetaStore | 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 |
| stPersistentTopLevelModuleNames | 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 |
| stPostFreshOpaqueId | 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 |
| 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 |
| stPostOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| stPostOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| stPostOpenMetaStore | 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 |
| stPostSolvedMetaStore | 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 |
| stPreCopiedNames | 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 |
| stPreImportedMetaStore | 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 |
| stPreNameCopies | 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 |
| strengthenS' | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| 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 |
| 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 |
| stringTCErr | Agda.TypeChecking.Errors |
| stringToArgName | Agda.Syntax.Common |
| stringToAttribute | Agda.Syntax.Concrete.Attribute |
| stringToRawName | Agda.Syntax.Common |
| 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.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 |
| stSolvedMetaStore | 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 |
| stTopLevelModuleNames | 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.Syntax.Common.Pretty |
| 2 (Type/Class) | Agda.Syntax.Common.Pretty |
| style | Agda.Syntax.Common.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.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 |
| 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 |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| 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 |
| 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 |
| szSortSize | Agda.TypeChecking.Substitute |
| szSortUniv | Agda.TypeChecking.Substitute |