| S | |
| 1 (Data Constructor) | Agda.Auto.Options |
| 2 (Type/Class) | Agda.TypeChecking.Serialise.Base |
| 3 (Type/Class) | Agda.Auto.Convert |
| 4 (Data Constructor) | Agda.Auto.Convert |
| safeFlag | Agda.Interaction.Options |
| SafeFlagEta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagEta_ | Agda.Interaction.Options.Warnings |
| SafeFlagInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagInjective_ | Agda.Interaction.Options.Warnings |
| SafeFlagNoCoverageCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagNoCoverageCheck_ | Agda.Interaction.Options.Warnings |
| SafeFlagNonTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagNonTerminating_ | Agda.Interaction.Options.Warnings |
| SafeFlagNoPositivityCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagNoPositivityCheck_ | Agda.Interaction.Options.Warnings |
| SafeFlagNoUniverseCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagNoUniverseCheck_ | Agda.Interaction.Options.Warnings |
| SafeFlagPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagPolarity_ | Agda.Interaction.Options.Warnings |
| SafeFlagPostulate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagPostulate_ | Agda.Interaction.Options.Warnings |
| SafeFlagPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagPragma_ | Agda.Interaction.Options.Warnings |
| SafeFlagTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagTerminating_ | Agda.Interaction.Options.Warnings |
| SafeFlagWithoutKFlagPrimEraseEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SafeFlagWithoutKFlagPrimEraseEquality_ | Agda.Interaction.Options.Warnings |
| SafeMode | Agda.Interaction.Options.Lenses |
| safePermute | Agda.Utils.Permutation |
| sameCohesion | Agda.Syntax.Common |
| sameDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sameHiding | Agda.Syntax.Common |
| sameModality | Agda.Syntax.Common |
| sameName | Agda.Syntax.Common |
| sameQuantity | Agda.Syntax.Common |
| sameRelevance | Agda.Syntax.Common |
| sameRoot | |
| 1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| sameVars | Agda.TypeChecking.Conversion |
| sanityCheckPragma | Agda.Compiler.MAlonzo.Pragmas |
| sanityCheckSubst | Agda.Syntax.Internal.SanityCheck |
| sanityCheckVars | Agda.Syntax.Internal.SanityCheck |
| sat | |
| 1 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| sat' | |
| 1 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| satNoPlaceholder | Agda.Syntax.Concrete.Operators.Parser |
| sayWhen | Agda.TypeChecking.Pretty.Call |
| sayWhere | Agda.TypeChecking.Pretty.Call |
| SBool | Agda.Utils.TypeLits |
| sccDAG | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| sccDAG' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| scCheckpoints | Agda.TypeChecking.Coverage |
| sccomcount | Agda.Auto.NarrowingSearch |
| sccs | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| sccs' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| scflip | Agda.Auto.NarrowingSearch |
| sChecked | Agda.Interaction.Response |
| SClause | Agda.TypeChecking.Coverage |
| sConsts | Agda.Auto.Convert |
| Scope | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base |
| 3 (Type/Class) | Agda.Utils.Warshall |
| ScopeCheck | Agda.Interaction.Imports |
| ScopeCheckDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| scopeCheckImport | Agda.Interaction.Imports |
| scopeCheckingSuffices | Agda.Compiler.Backend |
| ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ScopeCopyInfo | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| scopeCurrent | Agda.Syntax.Scope.Base |
| scopeDatatypeModule | Agda.Syntax.Scope.Base |
| ScopedDecl | Agda.Syntax.Abstract |
| ScopedExpr | Agda.Syntax.Abstract |
| scopedExpr | Agda.TypeChecking.Rules.Term |
| scopeFixities | Agda.Syntax.Scope.Base |
| 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 |
| Scoping | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| scPats | Agda.TypeChecking.Coverage |
| scsub1 | Agda.Auto.NarrowingSearch |
| scsub2 | Agda.Auto.NarrowingSearch |
| scSubst | Agda.TypeChecking.Coverage |
| scTarget | Agda.TypeChecking.Coverage |
| scTel | Agda.TypeChecking.Coverage |
| sCurMeta | Agda.Auto.Convert |
| searchAbout | Agda.Interaction.InteractionTop |
| secondPart | Agda.TypeChecking.Telescope |
| secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Section | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SectionApp | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sectIsSection | Agda.Syntax.Notation |
| sectKind | Agda.Syntax.Notation |
| sectLevel | Agda.Syntax.Notation |
| sectNotation | Agda.Syntax.Notation |
| seenUIds | Agda.Auto.Syntax |
| selectC | Agda.Interaction.Highlighting.Precise |
| Self | Agda.Compiler.JS.Syntax |
| self | Agda.Compiler.JS.Substitution |
| semi | Agda.Utils.Pretty |
| Semigroup | Agda.TypeChecking.Pretty |
| SemiRing | Agda.Utils.SemiRing |
| Semiring | |
| 1 (Type/Class) | Agda.Termination.Semiring |
| 2 (Data Constructor) | Agda.Termination.Semiring |
| sep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| SeqArg | |
| 1 (Type/Class) | Agda.Compiler.Treeless.Subst |
| 2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
| seqc | Agda.Auto.NarrowingSearch |
| seqctx | Agda.Auto.CaseSplit |
| seqP | Agda.Utils.Parser.MemoisedCPS |
| seqPO | Agda.Utils.PartialOrd |
| sEqs | Agda.Auto.Convert |
| sequenceListT | Agda.Utils.ListT |
| SerialisedRange | |
| 1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Common |
| 2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Common |
| Serialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| Set | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| set | Agda.Utils.Lens |
| setAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| setArgInfo | Agda.Syntax.Common |
| setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setAttribute | Agda.Syntax.Concrete.Attribute |
| setAttributes | Agda.Syntax.Concrete.Attribute |
| setBenchmarking | Agda.Utils.Benchmark |
| 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 |
| setContextPrecedence | Agda.Syntax.Scope.Monad |
| setCurrentModule | Agda.Syntax.Scope.Monad |
| setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setDebugging | Agda.TypeChecking.SizedTypes.Utils |
| setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setDefault | Agda.Utils.WithDefault |
| setErasedConArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setFoldl | Agda.TypeChecking.SizedTypes.WarshallSolver |
| setFreeVariables | Agda.Syntax.Common |
| setFreeVariablesArgInfo | Agda.Syntax.Common |
| setFunctionFlag | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setHiding | Agda.Syntax.Common |
| setHidingArgInfo | Agda.Syntax.Common |
| setImportedName | Agda.Syntax.Common |
| setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setIncludePaths | Agda.Interaction.Options.Lenses |
| setInput | Agda.Syntax.Parser.LookAhead |
| setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setInterface | Agda.Compiler.Common |
| setIntervalFile | Agda.Syntax.Position |
| setLastPos | Agda.Syntax.Parser.Monad |
| setLexInput | Agda.Syntax.Parser.Alex |
| setLibraryIncludes | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setLibraryPaths | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setLocalVars | Agda.Syntax.Scope.Monad |
| setMatchableSymbols | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setMetaArgInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setMetaNameSuggestion | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setMetaOccursCheck | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setModality | Agda.Syntax.Common |
| setModalityArgInfo | Agda.Syntax.Common |
| setModuleCheckpoint | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setMutual | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setMutualBlockInfo | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SetN | Agda.Syntax.Concrete |
| setNamedArg | Agda.Syntax.Common |
| setNamedScope | Agda.Syntax.Scope.Monad |
| setNameOf | Agda.Syntax.Common |
| setNameSpace | Agda.Syntax.Scope.Base |
| setNotInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setOrigin | Agda.Syntax.Common |
| setOriginArgInfo | Agda.Syntax.Common |
| setParsePos | Agda.Syntax.Parser.Monad |
| setPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setPersistentVerbosity | Agda.Interaction.Options.Lenses |
| setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setPragmaOptions | |
| 1 (Function) | Agda.Interaction.Options.Lenses |
| 2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setPrevToken | Agda.Syntax.Parser.Monad |
| setPristineAttribute | Agda.Syntax.Concrete.Attribute |
| setPristineAttributes | Agda.Syntax.Concrete.Attribute |
| setPristineCohesion | Agda.Syntax.Concrete.Attribute |
| setPristineQuantity | Agda.Syntax.Concrete.Attribute |
| setPristineRelevance | Agda.Syntax.Concrete.Attribute |
| setPtr | Agda.Utils.Pointer |
| setQuantity | Agda.Syntax.Common |
| setQuantityMod | Agda.Syntax.Common |
| SetRange | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setRange | Agda.Syntax.Position |
| setRelevance | Agda.Syntax.Common |
| setRelevanceMod | Agda.Syntax.Common |
| SetS | Agda.Syntax.Reflected |
| setSafeMode | Agda.Interaction.Options.Lenses |
| setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setScopeAccess | Agda.Syntax.Scope.Base |
| setScopeLocals | Agda.Syntax.Scope.Base |
| setSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setSplitTree | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SetToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
| setToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
| setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setTreeless | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setUsability | Agda.Termination.Order |
| setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| setVarsToBind | Agda.Syntax.Scope.Base |
| setVerbosity | Agda.Interaction.Options.Lenses |
| setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| several | Agda.Interaction.Highlighting.Precise |
| severalC | Agda.Interaction.Highlighting.Precise |
| SFalse | Agda.Utils.TypeLits |
| sgListT | Agda.Utils.ListT |
| sgMListT | Agda.Utils.ListT |
| SgTel | Agda.Syntax.Internal |
| sgTel | Agda.Syntax.Internal |
| ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShadowingInTelescope | |
| 1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| ShadowingInTelescope_ | Agda.Interaction.Options.Warnings |
| shadowLocal | Agda.Syntax.Scope.Base |
| sharing | Agda.Utils.Update |
| shift | Agda.Compiler.JS.Substitution |
| shifter | Agda.Compiler.JS.Substitution |
| shiftFrom | Agda.Compiler.JS.Substitution |
| ShouldBeApplicationOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBePath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBeRecordPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| shouldBeSort | Agda.TypeChecking.Sort, Agda.TypeChecking.CheckInternal |
| ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| shouldPostponeInstanceSearch | Agda.TypeChecking.InstanceArguments |
| shouldTryFastReduce | Agda.TypeChecking.Reduce |
| showA | Agda.Syntax.Abstract.Pretty |
| showATop | Agda.Syntax.Abstract.Pretty |
| showChar' | Agda.Syntax.Literal |
| showComputed | Agda.Interaction.BasicOps |
| showConstraints | Agda.Interaction.CommandLine |
| showContext | Agda.Interaction.CommandLine |
| showGoals | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop |
| ShowHead | Agda.TypeChecking.Rules.Decl |
| showHead | Agda.TypeChecking.Rules.Decl |
| ShowImplicitArgs | Agda.Interaction.Base |
| showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| showIndex | Agda.Utils.String |
| showInfoError | Agda.Interaction.EmacsTop |
| showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| showMetas | Agda.Interaction.CommandLine |
| showModuleContents | Agda.Interaction.InteractionTop |
| showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| showScope | Agda.Interaction.CommandLine |
| showString' | Agda.Syntax.Literal |
| showThousandSep | Agda.Utils.String |
| Sidecondition | Agda.Auto.NarrowingSearch |
| siFileType | Agda.Interaction.Imports |
| Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SigAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SigError | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sigError | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sigmaCon | Agda.TypeChecking.Primitive.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 |
| sigMName | Agda.Compiler.Common |
| Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SigUnknown | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| siModule | Agda.Interaction.Imports |
| siModuleName | Agda.Interaction.Imports |
| Simplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Simplified | Agda.Interaction.Base |
| Simplify | Agda.TypeChecking.Reduce |
| simplify | Agda.TypeChecking.Reduce |
| simplify' | Agda.TypeChecking.Reduce |
| simplify1 | Agda.TypeChecking.SizedTypes.Syntax |
| simplifyBlocked' | Agda.TypeChecking.Reduce |
| simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints |
| simplifyTTerm | Agda.Compiler.Treeless.Simplify |
| simplifyWithHypotheses | Agda.TypeChecking.SizedTypes.WarshallSolver |
| SingleClosed | Agda.TypeChecking.Level |
| singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SingleLevel | Agda.TypeChecking.Level |
| singleLevelView | Agda.TypeChecking.Level |
| SinglePlus | Agda.TypeChecking.Level |
| Singleton | Agda.Utils.Singleton |
| singleton | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Utils.Bag |
| 4 (Function) | Agda.Utils.IntSet.Infinite |
| 5 (Function) | Agda.Utils.Singleton |
| 6 (Function) | Agda.Utils.SmallSet |
| 7 (Function) | Agda.Utils.Trie |
| 8 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 9 (Function) | Agda.Interaction.Highlighting.Precise |
| singletonC | Agda.Interaction.Highlighting.Precise |
| 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.Utils.Pretty |
| siSource | Agda.Interaction.Imports |
| Size | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| size | |
| 1 (Function) | Agda.Utils.Bag |
| 2 (Function) | Agda.Utils.Size |
| 3 (Function) | Agda.Termination.SparseMatrix |
| sizeAndBoundVars | Agda.Auto.CaseSplit |
| sizeBuiltins | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeConst | Agda.Utils.Warshall |
| SizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
| sizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
| sizeContext | Agda.TypeChecking.SizedTypes.Solve |
| Sized | Agda.Utils.Size |
| sizedText | Agda.Utils.Pretty |
| SizedThing | |
| 1 (Type/Class) | Agda.Utils.Size |
| 2 (Data Constructor) | Agda.Utils.Size |
| sizedThing | Agda.Utils.Size |
| sizedTypesOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeExpr | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Utils.Warshall |
| sizeExpr | Agda.TypeChecking.SizedTypes.Solve |
| SizeExpr' | Agda.TypeChecking.SizedTypes.Syntax |
| sizeHypIds | Agda.TypeChecking.SizedTypes.Solve |
| sizeHypotheses | Agda.TypeChecking.SizedTypes.Solve |
| SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeLtSat | Agda.Interaction.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 (Data Constructor) | Agda.TypeChecking.SizedTypes |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
| 3 (Data Constructor) | Agda.TypeChecking.SizedTypes.Solve |
| sizeMetaArgs | Agda.TypeChecking.SizedTypes.Solve |
| sizeMetaId | Agda.TypeChecking.SizedTypes.Solve |
| sizePolarity | Agda.TypeChecking.Polarity |
| sizeRigid | Agda.Utils.Warshall |
| sizeSort | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeSucName | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeThing | Agda.Utils.Size |
| sizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeType_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeUniv | Agda.Syntax.Internal |
| sizeUniv | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeVar | Agda.Utils.Warshall |
| SizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeViewComparableWithMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeViewOffset | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeViewPred | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sizeViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Skip | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Compiler.Backend |
| skipBlock | Agda.Syntax.Parser.Comments |
| SleepingConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| slowNormaliseArgs | Agda.TypeChecking.Reduce |
| slowReduceTerm | Agda.TypeChecking.Reduce |
| sMainMeta | Agda.Auto.Convert |
| smallest | Agda.TypeChecking.SizedTypes.WarshallSolver |
| smallestPos | Agda.Interaction.Highlighting.Precise |
| smallestPosC | Agda.Interaction.Highlighting.Precise |
| SmallSet | Agda.Utils.SmallSet |
| smashTel | Agda.Syntax.Concrete.Pretty |
| sMetas | Agda.Auto.Convert |
| snd3 | Agda.Utils.Tuple |
| snoc | Agda.Utils.List |
| Sol | Agda.Auto.CaseSplit |
| Solution | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 3 (Type/Class) | Agda.Utils.Warshall |
| Solutions | Agda.Auto.Auto |
| solve | Agda.Utils.Warshall |
| solveAwakeConstraints | Agda.TypeChecking.Constraints |
| solveAwakeConstraints' | Agda.TypeChecking.Constraints |
| solveCluster | Agda.TypeChecking.SizedTypes.Solve |
| solveConstraint | Agda.TypeChecking.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 |
| 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 |
| solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| solvingProblems | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Some | |
| 1 (Type/Class) | Agda.Utils.IndexedList |
| 2 (Data Constructor) | Agda.Utils.IndexedList |
| SomeGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SomeKindsOfNames | Agda.Syntax.Scope.Base |
| someKindsOfNames | Agda.Syntax.Scope.Base |
| SomeWarnings | Agda.Interaction.Imports |
| SomeWhere | Agda.Syntax.Concrete |
| Sort | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Auto.Syntax |
| 3 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 4 (Type/Class) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Internal |
| 6 (Type/Class) | Agda.Syntax.Reflected |
| 7 (Data Constructor) | Agda.Syntax.Reflected |
| sort | Agda.Syntax.Internal |
| Sort' | Agda.Syntax.Internal |
| SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sortDefs | Agda.Compiler.Common |
| sorted | Agda.Utils.List |
| sortFitsIn | Agda.TypeChecking.Sort |
| SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sortInteractionPoints | Agda.Interaction.InteractionTop |
| sortOf | Agda.TypeChecking.Sort |
| source | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph |
| SourceFile | |
| 1 (Type/Class) | Agda.Interaction.FindFile |
| 2 (Data Constructor) | Agda.Interaction.FindFile |
| SourceInfo | |
| 1 (Type/Class) | Agda.Interaction.Imports |
| 2 (Data Constructor) | Agda.Interaction.Imports |
| sourceInfo | Agda.Interaction.Imports |
| sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| SourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| sourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| space | Agda.Utils.Pretty |
| spanAllowedBeforeModule | Agda.Syntax.Concrete |
| spanEnd | Agda.Utils.List |
| spanJust | Agda.Utils.List |
| SpecialCharacters | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Pretty |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Pretty |
| specialCharacters | Agda.Syntax.Concrete.Pretty |
| Specified | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SpeculateAbort | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SpeculateCommit | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| speculateMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SpeculateResult | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| speculateTCState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| speculateTCState_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SpineClause | Agda.Syntax.Abstract |
| SpineLHS | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| spineToLhs | Agda.Syntax.Abstract.Pattern |
| spineToLhsCore | Agda.Syntax.Abstract.Pattern |
| splashScreen | Agda.Interaction.CommandLine |
| spLhsDefName | Agda.Syntax.Abstract |
| spLhsInfo | Agda.Syntax.Abstract |
| spLhsPats | Agda.Syntax.Abstract |
| splitApplyElims | Agda.Syntax.Internal |
| splitArg | Agda.TypeChecking.Coverage.SplitTree |
| SplitAt | Agda.TypeChecking.Coverage.SplitTree |
| splitAtC | Agda.Interaction.Highlighting.Precise |
| splitBindings | Agda.TypeChecking.Coverage.SplitTree |
| splitC | Agda.TypeChecking.CompiledClause.Compile |
| SplitCatchall | Agda.TypeChecking.Coverage.SplitTree |
| SplitClause | Agda.TypeChecking.Coverage |
| splitClauses | Agda.TypeChecking.Coverage |
| splitClauseWithAbsurd | Agda.TypeChecking.Coverage |
| splitCommas | Agda.Interaction.Library.Parse |
| SplitCon | Agda.TypeChecking.Coverage.SplitTree |
| 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 |
| splitExactlyAt | Agda.Utils.List |
| splitExcludedLits | Agda.TypeChecking.Coverage.Match |
| splitLast | Agda.TypeChecking.Coverage |
| splitLazy | Agda.TypeChecking.Coverage.SplitTree |
| SplitLit | Agda.TypeChecking.Coverage.SplitTree |
| splitOffTrailingWithPatterns | Agda.Syntax.Abstract.Pattern |
| splitOn | Agda.TypeChecking.CompiledClause.Compile |
| splitOnDots | Agda.Syntax.Parser.Parser |
| SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SplitOnNonVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SplitOnUnusableCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| SplitPattern | Agda.TypeChecking.Coverage.Match |
| SplitPatVar | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
| splitPatVarIndex | Agda.TypeChecking.Coverage.Match |
| splitPatVarName | Agda.TypeChecking.Coverage.Match |
| splitPerm | Agda.TypeChecking.Telescope |
| splitResult | Agda.TypeChecking.Coverage |
| splitS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| splittableCohesion | Agda.TypeChecking.Irrelevance |
| SplitTag | Agda.TypeChecking.Coverage.SplitTree |
| SplitTel | |
| 1 (Type/Class) | Agda.TypeChecking.Telescope |
| 2 (Data Constructor) | Agda.TypeChecking.Telescope |
| splitTelescope | Agda.TypeChecking.Telescope |
| splitTelescopeAt | Agda.TypeChecking.Telescope |
| splitTelescopeExact | Agda.TypeChecking.Telescope |
| splitTelForWith | Agda.TypeChecking.With |
| SplittingDone | Agda.TypeChecking.Coverage.SplitTree |
| SplitTree | Agda.TypeChecking.Coverage.SplitTree |
| SplitTree' | Agda.TypeChecking.Coverage.SplitTree |
| SplitTreeLabel | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree |
| SplitTrees | Agda.TypeChecking.Coverage.SplitTree |
| splitTrees | Agda.TypeChecking.Coverage.SplitTree |
| SplitTrees' | Agda.TypeChecking.Coverage.SplitTree |
| square | Agda.Termination.SparseMatrix |
| Squash | Agda.Syntax.Common |
| src | Agda.TypeChecking.SizedTypes.WarshallSolver |
| SrcFile | Agda.Syntax.Position |
| srcFile | Agda.Syntax.Position |
| srcFilePath | Agda.Interaction.FindFile |
| srcNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| SRes | Agda.Auto.NarrowingSearch |
| sShowImplicitArguments | Agda.Interaction.Response |
| sSizeUniv | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| SSSMismatch | Agda.Utils.List |
| SSSResult | Agda.Utils.List |
| SSSStrip | Agda.Utils.List |
| St | |
| 1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
| 2 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
| stAccumStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Stack | Agda.TypeChecking.CompiledClause.Match |
| standardOptions | Agda.Interaction.Options |
| standardOptions_ | Agda.Interaction.Options |
| stAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| starP | Agda.Utils.Parser.MemoisedCPS |
| StarSemiRing | Agda.Utils.SemiRing |
| startPos | Agda.Syntax.Position |
| startPos' | Agda.Syntax.Position |
| 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 |
| 2 (Data Constructor) | Agda.Interaction.Response |
| status | Agda.Interaction.InteractionTop |
| stAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stealConstraintsTCM | Agda.TypeChecking.Constraints |
| stForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stImportedInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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 |
| 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 |
| stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Stmt | Agda.Utils.Haskell.Syntax |
| stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| storeDisambiguatedName | Agda.Interaction.Highlighting.Generate |
| stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPersistBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| stPostFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| stPostMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPostOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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 |
| stPostUsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreImportedInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| stPreLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPrePatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPrePatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPrePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stPreWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Str | |
| 1 (Type/Class) | Agda.Utils.String |
| 2 (Data Constructor) | Agda.Utils.String |
| Strengthen | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| strengthen | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| strengthenS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| Strict | Agda.Utils.Haskell.Syntax |
| Strictness | Agda.Utils.Haskell.Syntax |
| StrictPos | Agda.TypeChecking.Positivity.Occurrence |
| StrictSplit | Agda.TypeChecking.Coverage.SplitTree |
| String | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| string2HelpTopic | Agda.Interaction.Options.Help |
| string2WarningName | Agda.Interaction.Options.Warnings |
| stringC | Agda.TypeChecking.Serialise.Base |
| stringD | Agda.TypeChecking.Serialise.Base |
| stringE | Agda.TypeChecking.Serialise.Base |
| stringNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| stringParts | Agda.Syntax.Notation |
| stringTCErr | Agda.TypeChecking.Errors |
| stringToArgName | Agda.Syntax.Common |
| stringToAttribute | Agda.Syntax.Concrete.Attribute |
| stringToRawName | Agda.Syntax.Common |
| stripConstraintPids | Agda.Interaction.BasicOps |
| stripDontCare | Agda.Syntax.Internal |
| stripNoNames | Agda.Syntax.Scope.Monad |
| stripPrefixBy | Agda.Utils.List |
| stripReversedSuffix | Agda.Utils.List |
| stripRTS | Agda.Interaction.Options |
| stripSuffix | Agda.Utils.List |
| stripUnusedArguments | Agda.Compiler.Treeless.Unused |
| stripWithClausePatterns | Agda.TypeChecking.With |
| strMsg | Agda.Utils.Except |
| 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 |
| stShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stTCWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| StuckOn | Agda.Syntax.Internal |
| stuckOn | Agda.Syntax.Internal |
| 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 (Data Constructor) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.Utils.Pretty |
| style | Agda.Utils.Pretty |
| Sub | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
| sub | Agda.Auto.Syntax |
| SubConstraints | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| subi | Agda.Auto.Syntax |
| subLevel | Agda.TypeChecking.Level |
| Subscript | Agda.Utils.Suffix |
| subscriptAllowed | Agda.Utils.Suffix |
| Subst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| subst | |
| 1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Function) | Agda.Compiler.JS.Substitution |
| 3 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| subst' | Agda.Compiler.JS.Substitution |
| substBody | Agda.TypeChecking.CompiledClause.Compile |
| SubstCand | Agda.TypeChecking.MetaVars |
| SubstExpr | Agda.Syntax.Abstract |
| substExpr | Agda.Syntax.Abstract |
| Substitute | Agda.TypeChecking.SizedTypes.Syntax |
| substituter | Agda.Compiler.JS.Substitution |
| Substitution | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| Substitution' | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| substPattern | Agda.Syntax.Abstract.Pattern |
| substPattern' | Agda.Syntax.Abstract.Pattern |
| substUnder | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| SubstWithOrigin | Agda.TypeChecking.DisplayForm |
| substWithOrigin | Agda.TypeChecking.DisplayForm |
| subsvars | Agda.Auto.SearchControl |
| subtract | Agda.Utils.VarSet |
| subtypingForSizeLt | Agda.TypeChecking.MetaVars |
| subVar | Agda.TypeChecking.Free.Lazy |
| Suc | Agda.Utils.IndexedList |
| sucName | Agda.TypeChecking.Level |
| Suffix | |
| 1 (Type/Class) | Agda.Utils.Suffix |
| 2 (Type/Class) | Agda.Utils.List |
| suffixView | Agda.Utils.Suffix |
| Suggest | Agda.Syntax.Internal |
| Suggestion | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| suggestName | Agda.Syntax.Internal |
| suggests | Agda.Syntax.Internal |
| supremum | Agda.Termination.Order |
| supSize | Agda.Termination.SparseMatrix |
| swap | Agda.Utils.Tuple |
| swap01 | Agda.TypeChecking.Abstract |
| switchBenchmarking | Agda.Utils.Benchmark |
| SymArrow | Agda.Syntax.Parser.Tokens |
| SymAs | Agda.Syntax.Parser.Tokens |
| SymBar | Agda.Syntax.Parser.Tokens |
| Symbol | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Type/Class) | Agda.Syntax.Parser.Tokens |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| symbol | Agda.Syntax.Parser.LexActions |
| SymCloseBrace | Agda.Syntax.Parser.Tokens |
| SymCloseIdiomBracket | Agda.Syntax.Parser.Tokens |
| SymCloseParen | Agda.Syntax.Parser.Tokens |
| SymClosePragma | Agda.Syntax.Parser.Tokens |
| SymCloseVirtualBrace | Agda.Syntax.Parser.Tokens |
| SymColon | Agda.Syntax.Parser.Tokens |
| SymDot | Agda.Syntax.Parser.Tokens |
| SymDotDot | Agda.Syntax.Parser.Tokens |
| SymDoubleCloseBrace | Agda.Syntax.Parser.Tokens |
| SymDoubleOpenBrace | Agda.Syntax.Parser.Tokens |
| SymEllipsis | Agda.Syntax.Parser.Tokens |
| SymEmptyIdiomBracket | Agda.Syntax.Parser.Tokens |
| SymEndComment | Agda.Syntax.Parser.Tokens |
| SymEqual | Agda.Syntax.Parser.Tokens |
| SymLambda | Agda.Syntax.Parser.Tokens |
| SymOpenBrace | Agda.Syntax.Parser.Tokens |
| SymOpenIdiomBracket | Agda.Syntax.Parser.Tokens |
| SymOpenParen | Agda.Syntax.Parser.Tokens |
| SymOpenPragma | Agda.Syntax.Parser.Tokens |
| SymOpenVirtualBrace | Agda.Syntax.Parser.Tokens |
| SymQuestionMark | Agda.Syntax.Parser.Tokens |
| SymSemi | Agda.Syntax.Parser.Tokens |
| SymUnderscore | Agda.Syntax.Parser.Tokens |
| SymVirtualSemi | Agda.Syntax.Parser.Tokens |
| sync | Agda.Syntax.Parser.LookAhead |
| SynEq | Agda.TypeChecking.SyntacticEquality |
| Syntax | Agda.Syntax.Concrete |
| SyntaxBindingLambda | Agda.Syntax.Concrete |
| syntaxOf | Agda.Syntax.Notation |
| System | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.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 |