| S | |
| 1 (Type/Class) | Agda.Auto.Convert |
| 2 (Data Constructor) | Agda.Auto.Convert |
| SafeFlagNonTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SafeFlagNoTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SafeFlagPostulate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SafeFlagPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SafeFlagPrimTrustMe | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SafeFlagTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SafeMode | Agda.Interaction.Options.Lenses |
| safePermute | Agda.Utils.Permutation |
| Same | Agda.Compiler.Epic.Injection |
| sameDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| sameVars | Agda.TypeChecking.Conversion |
| sample | Agda.Utils.QuickCheck |
| sample' | Agda.Utils.QuickCheck |
| satisfy | Agda.Utils.ReadP |
| scale | Agda.Utils.QuickCheck |
| sccDAG | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| sccDAG' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 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.Utils.Warshall |
| 2 (Type/Class) | Agda.Syntax.Scope.Base |
| 3 (Data Constructor) | Agda.Syntax.Scope.Base |
| ScopeCheckDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| scopeCheckImport | Agda.Interaction.Imports |
| ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| scopeCurrent | Agda.Syntax.Scope.Base |
| scopeDatatypeModule | Agda.Syntax.Scope.Base |
| ScopedDecl | Agda.Syntax.Abstract |
| ScopedExpr | Agda.Syntax.Abstract |
| scopeImports | Agda.Syntax.Scope.Base |
| ScopeInfo | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base |
| scopeLocals | Agda.Syntax.Scope.Base |
| scopeLookup | Agda.Syntax.Scope.Base |
| scopeLookup' | Agda.Syntax.Scope.Base |
| ScopeM | 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 |
| scopePrecedence | Agda.Syntax.Scope.Base |
| Scoping | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| scPats | Agda.TypeChecking.Coverage |
| scPerm | 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 |
| secFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| secondPart | Agda.TypeChecking.Telescope |
| secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Section | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SectionApp | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Self | Agda.Compiler.JS.Syntax |
| self | Agda.Compiler.JS.Substitution |
| semi | Agda.Utils.Pretty |
| SemiRing | |
| 1 (Type/Class) | Agda.Utils.SemiRing |
| 2 (Type/Class) | Agda.Termination.Semiring |
| Semiring | |
| 1 (Type/Class) | Agda.Termination.Semiring |
| 2 (Data Constructor) | Agda.Termination.Semiring |
| semiringInvariant | Agda.Termination.Semiring |
| sep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| sepBy | Agda.Utils.ReadP |
| sepBy1 | Agda.Utils.ReadP |
| seqc | Agda.Auto.NarrowingSearch |
| seqctx | Agda.Auto.CaseSplit |
| seqPO | Agda.Utils.PartialOrd |
| sEqs | Agda.Auto.Convert |
| 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 |
| setArgColors | Agda.Syntax.Common |
| setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setBenchmarking | Agda.Utils.Benchmark |
| setBuiltinThings | Agda.TypeChecking.Monad.Builtin |
| setCommandLineOptions | |
| 1 (Function) | Agda.Interaction.Options.Lenses |
| 2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setCommandLineOptions' | Agda.Interaction.InteractionTop |
| setConName | Agda.Syntax.Internal |
| setContextPrecedence | Agda.Syntax.Scope.Monad |
| setCurrentModule | Agda.Syntax.Scope.Monad |
| setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
| setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| setFoldl | Agda.TypeChecking.SizedTypes.WarshallSolver |
| setFreqs | Agda.TypeChecking.Test.Generators |
| setHiding | Agda.Syntax.Common |
| setImportedSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setIncludeDirs | |
| 1 (Function) | Agda.Interaction.Options.Lenses |
| 2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setInput | Agda.Syntax.Parser.LookAhead |
| setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setInterface | Agda.Compiler.MAlonzo.Misc |
| setLastPos | Agda.Syntax.Parser.Monad |
| setLexInput | Agda.Syntax.Parser.Alex |
| setLocalVars | Agda.Syntax.Scope.Monad |
| setMetaNameSuggestion | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| setMutual | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| SetN | Agda.Syntax.Concrete |
| setNamedScope | Agda.Syntax.Scope.Monad |
| setNameSpace | Agda.Syntax.Scope.Base |
| SetOmegaNotValidType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setParsePos | Agda.Syntax.Parser.Monad |
| setPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setPersistentVerbosity | Agda.Interaction.Options.Lenses |
| setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setPragmaOptions | |
| 1 (Function) | Agda.Interaction.Options.Lenses |
| 2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setPrevToken | Agda.Syntax.Parser.Monad |
| setPtr | Agda.Utils.Pointer, Agda.Syntax.Internal |
| SetRange | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| setRange | Agda.Syntax.Position |
| setRelevance | Agda.Syntax.Common |
| setSafeMode | Agda.Interaction.Options.Lenses |
| setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setScopeAccess | Agda.Syntax.Scope.Base |
| setScopeLocals | Agda.Syntax.Scope.Base |
| setSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setTag | Agda.Compiler.Epic.Injection |
| setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| SetToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
| setToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
| setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| setVerbosity | Agda.Interaction.Options.Lenses |
| setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| several | Agda.Interaction.Highlighting.Precise |
| severalC | Agda.Interaction.Highlighting.Precise |
| sgListT | Agda.Utils.ListT |
| sgMListT | Agda.Utils.ListT |
| SgTel | Agda.Syntax.Internal |
| sgTel | Agda.Syntax.Internal |
| ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShadowedVar | Agda.Syntax.Scope.Base |
| shadowLocal | Agda.Syntax.Scope.Base |
| ShapeView | Agda.TypeChecking.Rules.LHS.Unify |
| shapeView | Agda.TypeChecking.Rules.LHS.Unify |
| shapeViewHH | Agda.TypeChecking.Rules.LHS.Unify |
| Shared | Agda.Syntax.Internal |
| shared | Agda.Syntax.Internal |
| sharedType | Agda.Syntax.Internal |
| 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 |
| ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeRecordPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| shouldEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| shouldReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| showA | Agda.Syntax.Abstract.Pretty |
| showATop | Agda.Syntax.Abstract.Pretty |
| showChar' | Agda.Syntax.Literal |
| showComparison | Agda.Interaction.BasicOps |
| showConstraints | Agda.Interaction.CommandLine |
| showContext | Agda.Interaction.CommandLine |
| ShowHead | Agda.TypeChecking.Rules.Decl |
| showHead | Agda.TypeChecking.Rules.Decl |
| ShowImplicitArgs | Agda.Interaction.InteractionTop |
| showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| showIndex | Agda.Utils.String |
| showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| showMetas | Agda.Interaction.CommandLine |
| showModuleContents | Agda.Interaction.InteractionTop |
| showOpenMetas | Agda.Interaction.InteractionTop |
| showPat' | Agda.TypeChecking.Pretty |
| showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| showScope | Agda.Interaction.CommandLine |
| showString' | Agda.Syntax.Literal |
| showThousandSep | Agda.Utils.String |
| shrink | Agda.Utils.QuickCheck |
| Shrink2 | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| ShrinkC | Agda.TypeChecking.Test.Generators |
| shrinkC | Agda.TypeChecking.Test.Generators |
| Shrinking | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| shrinking | Agda.Utils.QuickCheck |
| shrinkInit | Agda.Utils.QuickCheck |
| shrinkIntegral | Agda.Utils.QuickCheck |
| shrinkList | Agda.Utils.QuickCheck |
| shrinkNothing | Agda.Utils.QuickCheck |
| shrinkRealFrac | Agda.Utils.QuickCheck |
| shrinkRealFracToInteger | Agda.Utils.QuickCheck |
| ShrinkState | Agda.Utils.QuickCheck |
| shrinkState | Agda.Utils.QuickCheck |
| shuffle | Agda.Utils.QuickCheck |
| Sidecondition | Agda.Auto.NarrowingSearch |
| Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigMName | Agda.Compiler.MAlonzo.Misc |
| Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Simplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Simplified | Agda.Interaction.BasicOps |
| Simplify | Agda.TypeChecking.Reduce |
| simplify | Agda.TypeChecking.Reduce |
| simplify' | Agda.TypeChecking.Reduce |
| simplify1 | Agda.TypeChecking.SizedTypes.Syntax |
| simplifyBlocked' | Agda.TypeChecking.Reduce |
| simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints |
| simplifyWithHypotheses | Agda.TypeChecking.SizedTypes.WarshallSolver |
| singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| Singleton | Agda.Utils.Singleton |
| singleton | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Utils.HashMap |
| 4 (Function) | Agda.Utils.Singleton |
| 5 (Function) | Agda.Utils.Bag |
| 6 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 7 (Function) | Agda.Utils.Trie |
| 8 (Function) | Agda.Interaction.Highlighting.Precise |
| singletonC | Agda.Interaction.Highlighting.Precise |
| SingletonRecords | Agda.TypeChecking.MetaVars |
| singletonS | Agda.TypeChecking.Substitute |
| SingleVar | Agda.TypeChecking.Free.Lazy |
| Size | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| size | |
| 1 (Function) | Agda.Utils.HashMap |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.Size |
| 4 (Function) | Agda.Termination.SparseMatrix |
| SizeConst | Agda.Utils.Warshall |
| SizeConstraint | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
| sizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
| sizeContext | Agda.TypeChecking.SizedTypes.Solve |
| Sized | Agda.Utils.Size |
| sized | Agda.Utils.QuickCheck |
| SizedList | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| sizedText | Agda.Utils.Pretty |
| SizedThing | |
| 1 (Type/Class) | Agda.Utils.Size |
| 2 (Data Constructor) | Agda.Utils.Size |
| sizedThing | Agda.Utils.Size |
| SizeExpr | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Utils.Warshall |
| 3 (Type/Class) | Agda.TypeChecking.SizedTypes |
| sizeExpr | |
| 1 (Function) | Agda.TypeChecking.SizedTypes |
| 2 (Function) | 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 |
| sizeInvariant | Agda.Termination.SparseMatrix |
| SizeLtSat | Agda.Interaction.BasicOps |
| sizeMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeMaxView | Agda.TypeChecking.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 |
| sizePolarity | Agda.TypeChecking.Polarity |
| sizeRigid | Agda.Utils.Warshall |
| sizeSort | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeSucName | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeThing | Agda.Utils.Size |
| sizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeType_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeUniv | Agda.Syntax.Internal |
| sizeUniv | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeVar | Agda.Utils.Warshall |
| SizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeViewComparableWithMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeViewOffset | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeViewPred | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| Skip | Agda.Auto.Syntax |
| skipBlock | Agda.Syntax.Parser.Comments |
| skipMany | Agda.Utils.ReadP |
| skipMany1 | Agda.Utils.ReadP |
| skipSpaces | Agda.Utils.ReadP |
| sLub | Agda.TypeChecking.Substitute |
| sMainMeta | Agda.Auto.Convert |
| Small | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| 3 (Data Constructor) | Agda.Syntax.Common |
| smallest | Agda.TypeChecking.SizedTypes.WarshallSolver |
| smallestPos | Agda.Interaction.Highlighting.Precise |
| smallestPosC | Agda.Interaction.Highlighting.Precise |
| smallParams | Agda.TypeChecking.Rules.Data |
| Smart | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| smash'em | Agda.Compiler.Epic.Smashing |
| smashable | Agda.Compiler.Epic.Smashing |
| smashTel | Agda.Syntax.Concrete.Pretty |
| sMetas | Agda.Auto.Convert |
| snd3 | Agda.Utils.Tuple |
| Sol | Agda.Auto.CaseSplit |
| Solution | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Utils.Warshall |
| solve | |
| 1 (Function) | Agda.Utils.Warshall |
| 2 (Function) | Agda.Compiler.Epic.Injection |
| solveAwakeConstraints | Agda.TypeChecking.Constraints |
| solveAwakeConstraints' | Agda.TypeChecking.Constraints |
| solveCluster | Agda.TypeChecking.SizedTypes.Solve |
| solveConstraint | Agda.TypeChecking.Constraints |
| solveConstraint_ | Agda.TypeChecking.Constraints |
| SolvedButOpenHoles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| solveGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
| solveGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| solveSizeConstraints | |
| 1 (Function) | Agda.TypeChecking.SizedTypes |
| 2 (Function) | Agda.TypeChecking.SizedTypes.Solve |
| solveSizeConstraints_ | Agda.TypeChecking.SizedTypes.Solve |
| solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| SomeWarnings | Agda.Interaction.Imports |
| SomeWhere | Agda.Syntax.Concrete |
| Sort | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| 3 (Type/Class) | Agda.Auto.Syntax |
| 4 (Type/Class) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Internal |
| sort | Agda.Syntax.Internal |
| SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sorted | Agda.Utils.List |
| sortFreq | Agda.TypeChecking.Test.Generators |
| SortFreqs | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| sortFreqs | Agda.TypeChecking.Test.Generators |
| SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sortInteractionPoints | Agda.Interaction.InteractionTop |
| sortOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| SortSh | Agda.TypeChecking.Rules.LHS.Unify |
| sortTm | Agda.TypeChecking.Substitute |
| sortUniq | Agda.Utils.PartialOrd |
| source | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph |
| sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| SourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| space | Agda.Utils.Pretty |
| spanJust | Agda.Utils.List |
| spec_updateAt | Agda.Utils.List |
| spec_updateHead | Agda.Utils.List |
| spec_updateLast | Agda.Utils.List |
| SpineClause | Agda.Syntax.Abstract |
| SpineLHS | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| spineToLhs | Agda.Syntax.Abstract |
| spineToLhsCore | Agda.Syntax.Abstract |
| splashScreen | Agda.Interaction.CommandLine |
| spLhsDefName | Agda.Syntax.Abstract |
| spLhsInfo | Agda.Syntax.Abstract |
| spLhsPats | Agda.Syntax.Abstract |
| spLhsWithPats | Agda.Syntax.Abstract |
| Split | Agda.TypeChecking.Rules.LHS.Problem |
| splitApplyElims | Agda.Syntax.Internal |
| splitArg | Agda.TypeChecking.Coverage.SplitTree |
| splitAsNames | Agda.TypeChecking.Rules.LHS.Problem |
| SplitAt | Agda.TypeChecking.Coverage.SplitTree |
| splitAtC | Agda.Interaction.Highlighting.Precise |
| splitBindings | Agda.TypeChecking.Coverage.SplitTree |
| splitC | Agda.TypeChecking.CompiledClause.Compile |
| SplitClause | Agda.TypeChecking.Coverage |
| splitClauses | Agda.TypeChecking.Coverage |
| splitClauseWithAbsurd | Agda.TypeChecking.Coverage |
| SplitError | |
| 1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| splitExactlyAt | Agda.Utils.List |
| splitFocus | Agda.TypeChecking.Rules.LHS.Problem |
| splitLast | Agda.TypeChecking.Coverage |
| splitLPats | Agda.TypeChecking.Rules.LHS.Problem |
| splitOn | Agda.TypeChecking.CompiledClause.Compile |
| SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| splitPerm | Agda.TypeChecking.Telescope |
| SplitProblem | Agda.TypeChecking.Rules.LHS.Problem |
| splitProblem | Agda.TypeChecking.Rules.LHS.Split |
| splitProjection | Agda.TypeChecking.Rules.LHS.Problem |
| SplitRest | Agda.TypeChecking.Rules.LHS.Problem |
| splitRestType | Agda.TypeChecking.Rules.LHS.Problem |
| splitResult | Agda.TypeChecking.Coverage |
| splitRPats | Agda.TypeChecking.Rules.LHS.Problem |
| splitS | Agda.TypeChecking.Substitute |
| SplitTel | |
| 1 (Type/Class) | Agda.TypeChecking.Telescope |
| 2 (Data Constructor) | Agda.TypeChecking.Telescope |
| splitTelescope | Agda.TypeChecking.Telescope |
| SplittingDone | Agda.TypeChecking.Coverage.SplitTree |
| SplitTree | Agda.TypeChecking.Coverage.SplitTree |
| SplitTree' | Agda.TypeChecking.Coverage.SplitTree |
| SplitTreeLabel | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree |
| SplitTrees | Agda.TypeChecking.Coverage.SplitTree |
| splitTrees | Agda.TypeChecking.Coverage.SplitTree |
| SplitTrees' | Agda.TypeChecking.Coverage.SplitTree |
| square | Agda.Termination.SparseMatrix |
| src | Agda.TypeChecking.SizedTypes.WarshallSolver |
| srcFile | Agda.Syntax.Position |
| srcNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| SRes | Agda.Auto.NarrowingSearch |
| sShowImplicitArguments | Agda.Interaction.Response |
| sSuc | Agda.Syntax.Internal |
| stAccumStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Stack | Agda.TypeChecking.CompiledClause.Match |
| standardOptions | Agda.Interaction.Options |
| standardOptions_ | Agda.Interaction.Options |
| StarSemiRing | Agda.Utils.SemiRing |
| startPos | Agda.Syntax.Position |
| StaticPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Statistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| stBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stdArgs | Agda.Utils.QuickCheck |
| stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| step | Agda.Compiler.Epic.Erasure |
| stFreshCtxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| storeDisambiguatedName | Agda.Interaction.Highlighting.Generate |
| stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostFreshCtxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPostSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPrePatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPrePatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPrePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPreVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Str | |
| 1 (Type/Class) | Agda.Utils.String |
| 2 (Data Constructor) | Agda.Utils.String |
| Strengthen | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| strengthen | Agda.TypeChecking.Substitute |
| StrictPos | Agda.TypeChecking.Positivity.Occurrence |
| String | |
| 1 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| string | Agda.Utils.ReadP |
| stringChr | Agda.Compiler.JS.Parser |
| stringLit | Agda.Compiler.JS.Parser |
| stringNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| stringParts | Agda.Syntax.Notation |
| stringStr | Agda.Compiler.JS.Parser |
| stringToArgName | Agda.Syntax.Internal |
| stringToMyId | Agda.Auto.Syntax |
| stringToRawName | Agda.Syntax.Common |
| stripDontCare | Agda.Syntax.Internal |
| stripNoNames | Agda.Syntax.Scope.Monad |
| stripWithClausePatterns | Agda.TypeChecking.With |
| strMsg | Agda.Utils.Except |
| strongly | Agda.TypeChecking.MetaVars.Occurs |
| StronglyRigid | |
| 1 (Data Constructor) | Agda.TypeChecking.Free.Lazy |
| 2 (Data Constructor) | Agda.TypeChecking.Free |
| 3 (Data Constructor) | Agda.TypeChecking.Free.Old |
| 4 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| StronglyRigidOccurrence | Agda.TypeChecking.Rules.LHS.Unify |
| stronglyRigidVars | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| StuckOn | Agda.Syntax.Internal |
| stuckOn | Agda.Syntax.Internal |
| stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Style | |
| 1 (Data Constructor) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.Utils.Pretty |
| style | Agda.Utils.Pretty |
| Sub | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
| 3 (Type/Class) | Agda.TypeChecking.Rules.LHS.Unify |
| sub | Agda.Auto.Syntax |
| SubConstraints | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| subi | Agda.Auto.Syntax |
| sublistOf | Agda.Utils.QuickCheck |
| Subscript | Agda.Utils.Suffix |
| Subst | Agda.TypeChecking.Substitute |
| subst | |
| 1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Function) | Agda.Compiler.JS.Substitution |
| 3 (Function) | Agda.Compiler.Epic.AuxAST |
| 4 (Function) | Agda.TypeChecking.Substitute |
| subst' | Agda.Compiler.JS.Substitution |
| substBody | Agda.TypeChecking.CompiledClause.Compile |
| substBranch | Agda.Compiler.Epic.AuxAST |
| SubstCand | Agda.TypeChecking.MetaVars |
| SubstExpr | Agda.Syntax.Abstract |
| substExpr | Agda.Syntax.Abstract |
| substForDot | Agda.Compiler.Epic.Injection |
| SubstHH | Agda.TypeChecking.Rules.LHS.Unify |
| substHH | Agda.TypeChecking.Rules.LHS.Unify |
| Substitute | Agda.TypeChecking.SizedTypes.Syntax |
| substituter | Agda.Compiler.JS.Substitution |
| Substitution | |
| 1 (Type/Class) | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| 2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| substLit | Agda.Compiler.Epic.FromAgda |
| substPattern | Agda.Syntax.Abstract |
| substs | Agda.Compiler.Epic.AuxAST |
| substTerm | Agda.Compiler.Epic.FromAgda |
| substUnder | Agda.TypeChecking.Substitute |
| substUnderHH | Agda.TypeChecking.Rules.LHS.Unify |
| subsvars | Agda.Auto.SearchControl |
| subterms | Agda.Utils.QuickCheck |
| subtract | Agda.Utils.VarSet |
| subtypingForSizeLt | Agda.TypeChecking.MetaVars |
| Success | Agda.Utils.QuickCheck |
| suchThat | Agda.Utils.QuickCheck |
| suchThatMaybe | Agda.Utils.QuickCheck |
| sucName | Agda.TypeChecking.Level |
| Suffix | |
| 1 (Type/Class) | Agda.Utils.Suffix |
| 2 (Type/Class) | Agda.Utils.List |
| suffixView | Agda.Utils.Suffix |
| Suggest | Agda.Syntax.Internal |
| suggest | Agda.Syntax.Internal |
| supremum | Agda.Termination.Order |
| swap | Agda.Utils.Tuple |
| switchBenchmarking | Agda.Utils.Benchmark |
| SymArrow | Agda.Syntax.Parser.Tokens |
| SymAs | Agda.Syntax.Parser.Tokens |
| SymBar | Agda.Syntax.Parser.Tokens |
| Symbol | |
| 1 (Type/Class) | Agda.Syntax.Parser.Tokens |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| symbol | Agda.Syntax.Parser.LexActions |
| SymCloseBrace | Agda.Syntax.Parser.Tokens |
| SymCloseParen | Agda.Syntax.Parser.Tokens |
| SymClosePragma | Agda.Syntax.Parser.Tokens |
| SymCloseVirtualBrace | Agda.Syntax.Parser.Tokens |
| SymColon | Agda.Syntax.Parser.Tokens |
| SymDot | Agda.Syntax.Parser.Tokens |
| SymDotDot | Agda.Syntax.Parser.Tokens |
| SymDoubleCloseBrace | Agda.Syntax.Parser.Tokens |
| SymDoubleOpenBrace | Agda.Syntax.Parser.Tokens |
| SymEllipsis | Agda.Syntax.Parser.Tokens |
| SymEndComment | Agda.Syntax.Parser.Tokens |
| SymEqual | Agda.Syntax.Parser.Tokens |
| SymLambda | Agda.Syntax.Parser.Tokens |
| SymOpenBrace | Agda.Syntax.Parser.Tokens |
| SymOpenParen | Agda.Syntax.Parser.Tokens |
| SymOpenPragma | Agda.Syntax.Parser.Tokens |
| SymOpenVirtualBrace | Agda.Syntax.Parser.Tokens |
| SymQuestionMark | Agda.Syntax.Parser.Tokens |
| SymSemi | Agda.Syntax.Parser.Tokens |
| SymUnderscore | Agda.Syntax.Parser.Tokens |
| SymVirtualSemi | Agda.Syntax.Parser.Tokens |
| sync | Agda.Syntax.Parser.LookAhead |
| SynEq | Agda.TypeChecking.SyntacticEquality |
| Syntax | Agda.Syntax.Concrete |
| SyntaxBindingLambda | Agda.Syntax.Concrete |
| syntaxOf | Agda.Syntax.Fixity |