| S | |
| 1 (Type/Class) | Agda.Auto.Convert |
| 2 (Data Constructor) | Agda.Auto.Convert |
| 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 |
| Same | Agda.Compiler.Epic.Injection |
| sameVars | Agda.TypeChecking.Conversion |
| sample | Agda.Utils.QuickCheck |
| sample' | Agda.Utils.QuickCheck |
| satisfy | Agda.Utils.ReadP |
| sccomcount | Agda.Auto.NarrowingSearch |
| sccs | Agda.Utils.Graph |
| sccs' | Agda.Utils.Graph |
| 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 |
| scopeParents | Agda.Syntax.Scope.Base |
| scopePrecedence | Agda.Syntax.Scope.Base |
| 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 |
| sEqs | Agda.Auto.Convert |
| Set | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| set | Agda.Syntax.Internal |
| set0 | Agda.Syntax.Internal |
| setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setBuiltinThings | Agda.TypeChecking.Monad.Builtin |
| setCommandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setCommandLineOptions' | Agda.Interaction.InteractionTop |
| 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 |
| setExtLambdaTele | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setFreqs | Agda.TypeChecking.Test.Generators |
| setImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setInput | Agda.Syntax.Parser.LookAhead |
| setInputFile | Agda.TypeChecking.Monad.Options, 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 |
| 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 |
| setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setPragmaOptions | 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 |
| setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setScopeAccess | Agda.Syntax.Scope.Base |
| setSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setTag | Agda.Compiler.Epic.Injection |
| setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| several | Agda.Interaction.Highlighting.Precise |
| severalC | Agda.Interaction.Highlighting.Precise |
| ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| 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.Concrete.Pretty |
| showComparison | Agda.Interaction.BasicOps |
| showConstraints | Agda.Interaction.CommandLine.CommandLine |
| showContext | Agda.Interaction.CommandLine.CommandLine |
| 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.CommandLine |
| showModuleContents | Agda.Interaction.InteractionTop |
| showPat | Agda.TypeChecking.With |
| showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| showScope | Agda.Interaction.CommandLine.CommandLine |
| showString' | Agda.Syntax.Concrete.Pretty |
| 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 |
| shrinkNothing | Agda.Utils.QuickCheck |
| shrinkRealFrac | Agda.Utils.QuickCheck |
| ShrinkState | Agda.Utils.QuickCheck |
| shrinkState | 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 |
| sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints |
| singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| singleton | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.HashMap |
| 3 (Function) | Agda.Utils.Trie |
| 4 (Function) | Agda.Utils.Graph |
| 5 (Function) | Agda.Interaction.Highlighting.Precise |
| singletonC | Agda.Interaction.Highlighting.Precise |
| SingletonRecords | Agda.TypeChecking.MetaVars |
| singletonS | Agda.TypeChecking.Substitute |
| Size | |
| 1 (Type/Class) | Agda.Termination.Matrix |
| 2 (Data Constructor) | Agda.Termination.Matrix |
| 3 (Type/Class) | Agda.Termination.SparseMatrix |
| 4 (Data Constructor) | Agda.Termination.SparseMatrix |
| size | |
| 1 (Function) | Agda.Utils.HashMap |
| 2 (Function) | Agda.Termination.Matrix |
| 3 (Function) | Agda.Utils.Size |
| 4 (Function) | Agda.Termination.SparseMatrix |
| 5 (Function) | Agda.Termination.Lexicographic |
| SizeConst | Agda.Utils.Warshall |
| SizeConstraint | Agda.TypeChecking.SizedTypes |
| 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 |
| SizeExpr | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes |
| sizeExpr | Agda.TypeChecking.SizedTypes |
| SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeInvariant | |
| 1 (Function) | Agda.Termination.Matrix |
| 2 (Function) | Agda.Termination.SparseMatrix |
| sizeMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeMaxView | Agda.TypeChecking.SizedTypes |
| SizeMeta | Agda.TypeChecking.SizedTypes |
| sizePolarity | Agda.TypeChecking.Polarity |
| sizeRigid | Agda.Utils.Warshall |
| 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 |
| sizeType | 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 |
| smallestPos | Agda.Interaction.Highlighting.Precise |
| smallestPosC | Agda.Interaction.Highlighting.Precise |
| 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 | Agda.Utils.Warshall |
| solve | |
| 1 (Function) | Agda.Utils.Warshall |
| 2 (Function) | Agda.Compiler.Epic.Injection |
| solveAwakeConstraints | Agda.TypeChecking.Constraints |
| solveAwakeConstraints' | Agda.TypeChecking.Constraints |
| solveConstraint | Agda.TypeChecking.Constraints |
| solveConstraint_ | Agda.TypeChecking.Constraints |
| solveIrrelevantMetas | Agda.TypeChecking.InstanceArguments |
| solveMetaIfIrrelevant | Agda.TypeChecking.InstanceArguments |
| solveSizeConstraints | Agda.TypeChecking.SizedTypes |
| solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| 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 |
| 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 |
| source | Agda.Termination.CallGraph |
| SourceToModule | Agda.Interaction.FindFile |
| sourceToModule | Agda.Interaction.FindFile |
| space | Agda.Utils.Pretty |
| SpineLHS | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| splashScreen | Agda.Interaction.CommandLine.CommandLine |
| spLhsDefName | Agda.Syntax.Abstract |
| spLhsInfo | Agda.Syntax.Abstract |
| spLhsPats | Agda.Syntax.Abstract |
| spLhsWithPats | Agda.Syntax.Abstract |
| Split | Agda.TypeChecking.Rules.LHS.Problem |
| split | Agda.TypeChecking.Coverage |
| split' | Agda.TypeChecking.Coverage |
| 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 |
| SplitClause | Agda.TypeChecking.Coverage |
| splitClauses | Agda.TypeChecking.Coverage |
| splitClauseWithAbs | Agda.TypeChecking.Coverage |
| splitDbIndexToLevel | Agda.TypeChecking.Coverage |
| SplitError | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Type/Class) | Agda.TypeChecking.Coverage |
| splitLast | Agda.TypeChecking.Coverage |
| splitOn | Agda.TypeChecking.CompiledClause.Compile |
| SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SplitPanic | Agda.TypeChecking.Rules.LHS.Problem |
| splitPerm | Agda.TypeChecking.Telescope |
| SplitProblem | Agda.TypeChecking.Rules.LHS.Problem |
| splitProblem | Agda.TypeChecking.Rules.LHS.Split |
| splitS | Agda.TypeChecking.Substitute |
| splitStrategy | Agda.TypeChecking.Coverage |
| SplitTel | |
| 1 (Type/Class) | Agda.TypeChecking.Telescope |
| 2 (Data Constructor) | Agda.TypeChecking.Telescope |
| splitTelescope | Agda.TypeChecking.Telescope |
| SplittingDone | Agda.TypeChecking.Coverage.SplitTree |
| splitTrailingImplicits | Agda.TypeChecking.Rules.Def |
| 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 | |
| 1 (Function) | Agda.Termination.Matrix |
| 2 (Function) | Agda.Termination.SparseMatrix |
| srcFile | Agda.Syntax.Position |
| SRes | Agda.Auto.NarrowingSearch |
| sShowImplicitArguments | Agda.Interaction.Response |
| sSuc | Agda.Syntax.Internal |
| Stack | Agda.TypeChecking.CompiledClause.Match |
| standardOptions_ | Agda.Interaction.Options |
| 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 |
| 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 |
| stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| step | Agda.Compiler.Epic.Erasure |
| stExtLambdaTele | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stFreshThings | 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 |
| 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 |
| stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPersistent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Str | |
| 1 (Type/Class) | Agda.Utils.QuickCheck |
| 2 (Data Constructor) | Agda.Utils.Pretty |
| 3 (Type/Class) | Agda.TypeChecking.Primitive |
| 4 (Data Constructor) | Agda.TypeChecking.Primitive |
| StrictPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| stringParts | Agda.Syntax.Notation |
| stringStr | Agda.Compiler.JS.Parser |
| stripDontCare | Agda.Syntax.Internal |
| stripNoNames | Agda.Syntax.Scope.Monad |
| stripWithClausePatterns | Agda.TypeChecking.With |
| strongly | Agda.TypeChecking.MetaVars.Occurs |
| StronglyRigid | |
| 1 (Data Constructor) | Agda.TypeChecking.Free |
| 2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| StronglyRigidOccurrence | Agda.TypeChecking.Rules.LHS.Unify |
| stronglyRigidVars | Agda.TypeChecking.Free |
| 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 |
| stTermErrs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Style | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Data Constructor) | Agda.Utils.Pretty |
| style | Agda.Utils.Pretty |
| Sub | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (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 |
| Subscript | Agda.Utils.Suffix |
| Subst | Agda.TypeChecking.Substitute |
| subst | |
| 1 (Function) | Agda.Compiler.JS.Substitution |
| 2 (Function) | Agda.Compiler.Epic.AuxAST |
| 3 (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 |
| substForDot | Agda.Compiler.Epic.Injection |
| SubstHH | Agda.TypeChecking.Rules.LHS.Unify |
| substHH | Agda.TypeChecking.Rules.LHS.Unify |
| substituter | Agda.Compiler.JS.Substitution |
| Substitution | |
| 1 (Type/Class) | Agda.TypeChecking.Substitute |
| 2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| substLetBinding | Agda.Syntax.Abstract |
| substLit | Agda.Compiler.Epic.FromAgda |
| substPattern | Agda.Syntax.Abstract |
| substs | Agda.Compiler.Epic.AuxAST |
| substTerm | Agda.Compiler.Epic.FromAgda |
| substTypedBinding | Agda.Syntax.Abstract |
| substTypedBindings | Agda.Syntax.Abstract |
| substUnder | Agda.TypeChecking.Substitute |
| substUnderHH | Agda.TypeChecking.Rules.LHS.Unify |
| subsvars | Agda.Auto.SearchControl |
| subtract | Agda.Utils.VarSet |
| Success | Agda.Utils.QuickCheck |
| suchThat | Agda.Utils.QuickCheck |
| suchThatMaybe | Agda.Utils.QuickCheck |
| sucName | Agda.TypeChecking.Level |
| Suffix | |
| 1 (Type/Class) | Agda.Utils.List |
| 2 (Type/Class) | Agda.Utils.Suffix |
| suffixView | Agda.Utils.Suffix |
| supremum | Agda.Termination.CallGraph |
| SymArrow | Agda.Syntax.Parser.Tokens |
| SymAs | Agda.Syntax.Parser.Tokens |
| SymBar | Agda.Syntax.Parser.Tokens |
| Symbol | |
| 1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 2 (Type/Class) | Agda.Syntax.Parser.Tokens |
| 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 |
| 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 |
| Syntax | Agda.Syntax.Concrete |
| SyntaxBindingLambda | Agda.Syntax.Concrete |
| syntaxOf | Agda.Syntax.Fixity |