S | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
2 (Data Constructor) | Agda.Mimer.Options |
safeButNotBuiltin | Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions |
safeFlag | Agda.Interaction.Options |
SafeFlagEta | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagEta_ | Agda.Interaction.Options.Warnings |
SafeFlagInjective | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagInjective_ | Agda.Interaction.Options.Warnings |
SafeFlagNoCoverageCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagNoCoverageCheck_ | Agda.Interaction.Options.Warnings |
SafeFlagNonTerminating | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagNonTerminating_ | Agda.Interaction.Options.Warnings |
SafeFlagNoPositivityCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagNoPositivityCheck_ | Agda.Interaction.Options.Warnings |
SafeFlagNoUniverseCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagNoUniverseCheck_ | Agda.Interaction.Options.Warnings |
SafeFlagPolarity | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagPolarity_ | Agda.Interaction.Options.Warnings |
SafeFlagPostulate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SafeFlagPostulate_ | Agda.Interaction.Options.Warnings |
SafeFlagPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SafeFlagPragma_ | Agda.Interaction.Options.Warnings |
SafeFlagTerminating | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
SafeFlagTerminating_ | Agda.Interaction.Options.Warnings |
SafeFlagWithoutKFlagPrimEraseEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SafeFlagWithoutKFlagPrimEraseEquality_ | Agda.Interaction.Options.Warnings |
SafeMode | Agda.Interaction.Options.Lenses |
sameCohesion | Agda.Syntax.Common |
sameDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sameErased | Agda.Syntax.Common |
sameFile | Agda.Utils.FileName |
sameHiding | Agda.Syntax.Common |
sameKind | Agda.Syntax.Concrete.Definitions.Types |
sameModality | Agda.Syntax.Common |
sameName | Agda.Syntax.Common |
sameQuantity | Agda.Syntax.Common |
sameRelevance | Agda.Syntax.Common |
sameRoot | |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
sameVars | Agda.TypeChecking.Conversion |
sanityCheckPragma | Agda.Compiler.MAlonzo.Pragmas |
sanityCheckSubst | Agda.Syntax.Internal.SanityCheck |
sanityCheckVars | Agda.Syntax.Internal.SanityCheck |
sat | |
1 (Function) | Agda.Utils.Parser.MemoisedCPS |
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
sat' | |
1 (Function) | Agda.Utils.Parser.MemoisedCPS |
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
satNoPlaceholder | Agda.Syntax.Concrete.Operators.Parser |
saturateOpaqueBlocks | Agda.TypeChecking.Opacity |
sayWhen | Agda.TypeChecking.Pretty.Call |
sayWhere | Agda.TypeChecking.Pretty.Call |
SBool | Agda.Utils.TypeLits |
scanl | Agda.Utils.List1 |
scanl1 | Agda.Utils.List1 |
scanr | Agda.Utils.List1 |
scanr1 | Agda.Utils.List1 |
scatterMP | Agda.Utils.Monad |
sccDAG | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
sccDAG' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
scCheckpoints | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
sccs | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
sccs' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
sChecked | Agda.Interaction.Response.Base, Agda.Interaction.Response |
SClause | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
Scope | |
1 (Type/Class) | Agda.Syntax.Scope.Base |
2 (Data Constructor) | Agda.Syntax.Scope.Base |
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.Base, Agda.Compiler.Backend |
ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ScopeCopyInfo | |
1 (Type/Class) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Abstract |
scopeCurrent | Agda.Syntax.Scope.Base |
scopeDatatypeModule | Agda.Syntax.Scope.Base |
ScopedDecl | Agda.Syntax.Abstract |
ScopedDeclS | Agda.Syntax.Abstract |
ScopedExpr | Agda.Syntax.Abstract |
scopedExpr | Agda.TypeChecking.Rules.Term |
scopeFixities | Agda.Syntax.Scope.Base |
scopeFixitiesAndPolarities | Agda.Syntax.Scope.Base |
scopeImports | Agda.Syntax.Scope.Base |
ScopeInfo | |
1 (Type/Class) | Agda.Syntax.Scope.Base |
2 (Data Constructor) | Agda.Syntax.Scope.Base |
scopeInScope | Agda.Syntax.Scope.Base |
scopeInverseModule | Agda.Syntax.Scope.Base |
scopeInverseName | Agda.Syntax.Scope.Base |
scopeLocals | Agda.Syntax.Scope.Base |
scopeLookup | Agda.Syntax.Scope.Base |
scopeLookup' | Agda.Syntax.Scope.Base |
ScopeM | Agda.Syntax.Scope.Monad |
ScopeMemo | |
1 (Type/Class) | Agda.Syntax.Scope.Monad |
2 (Data Constructor) | Agda.Syntax.Scope.Monad |
scopeModules | Agda.Syntax.Scope.Base |
scopeName | Agda.Syntax.Scope.Base |
scopeNameSpace | Agda.Syntax.Scope.Base |
ScopeNameSpaces | Agda.Syntax.Scope.Base |
scopeNameSpaces | Agda.Syntax.Scope.Base |
scopeParents | Agda.Syntax.Scope.Base |
scopePolarities | Agda.Syntax.Scope.Base |
scopePrecedence | Agda.Syntax.Scope.Base |
scopeVarsToBind | Agda.Syntax.Scope.Base |
scopeWarning | Agda.Syntax.Scope.Monad |
scopeWarning' | Agda.Syntax.Scope.Monad |
Scoping | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
scPats | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
scSubst | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
scTarget | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
scTel | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
searchAbout | Agda.Interaction.InteractionTop |
secondPart | Agda.TypeChecking.Telescope |
secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Section | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SectionApp | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
SectionS | Agda.Syntax.Abstract |
Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sectIsSection | Agda.Syntax.Notation |
sectKind | Agda.Syntax.Notation |
sectLevel | Agda.Syntax.Notation |
sectNotation | Agda.Syntax.Notation |
Self | Agda.Compiler.JS.Syntax |
self | Agda.Compiler.JS.Substitution |
semi | Agda.Syntax.Common.Pretty |
Semigroup | Agda.Utils.Semigroup, Agda.TypeChecking.Pretty |
SemiRing | Agda.Utils.SemiRing |
Semiring | |
1 (Type/Class) | Agda.Termination.Semiring |
2 (Data Constructor) | Agda.Termination.Semiring |
sep | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
SeqArg | |
1 (Type/Class) | Agda.Compiler.Treeless.Subst |
2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
seqP | Agda.Utils.Parser.MemoisedCPS |
seqPO | Agda.Utils.PartialOrd |
sequenceListT | Agda.Utils.ListT |
Sequential | Agda.Compiler.ToTreeless |
SerialisedRange | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Common |
2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Common |
Serialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
Serialize | Agda.Utils.ProfileOptions |
Series | Agda.Interaction.JSON |
set | Agda.Utils.Lens |
setAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
setAnnotation | Agda.Syntax.Common |
setArgInfo | Agda.Syntax.Common |
setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setAttribute | Agda.Syntax.Concrete.Attribute |
setAttributes | Agda.Syntax.Concrete.Attribute |
setBenchmarking | Agda.Utils.Benchmark |
SetBindingSite | Agda.Syntax.Scope.Base |
setBindingSite | Agda.Syntax.Scope.Base |
setBlockingVarOverlap | Agda.TypeChecking.Coverage.Match |
setBuiltinThings | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setCohesion | Agda.Syntax.Common |
setCohesionMod | Agda.Syntax.Common |
setCommandLineOptions | |
1 (Function) | Agda.Interaction.Options.Lenses |
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setCommandLineOptions' | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setCommandLineOpts | Agda.Interaction.InteractionTop |
setCompiledArgUse | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setCompiledClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setConName | Agda.Syntax.Internal |
setContext | Agda.Syntax.Parser.Monad |
setContextPrecedence | Agda.Syntax.Scope.Monad |
setCurrentModule | Agda.Syntax.Scope.Monad |
setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setDebugging | Agda.TypeChecking.SizedTypes.Utils |
setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setDefault | Agda.Utils.WithDefault |
setErasedConArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setFoldl | Agda.TypeChecking.SizedTypes.WarshallSolver |
setFreeVariables | Agda.Syntax.Common |
setFreeVariablesArgInfo | Agda.Syntax.Common |
setFunctionFlag | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setHardCompileTimeModeIfErased | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setHardCompileTimeModeIfErased' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setHiding | Agda.Syntax.Common |
setHidingArgInfo | Agda.Syntax.Common |
setImportedName | Agda.Syntax.Common |
setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setIncludePaths | Agda.Interaction.Options.Lenses |
setInput | Agda.Syntax.Parser.LookAhead |
setInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setInterface | Agda.Compiler.Common |
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 |
setLock | Agda.Syntax.Common |
setMatchableSymbols | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setMetaGeneralizableArgInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setMetaNameSuggestion | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setMetaOccursCheck | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setModality | Agda.Syntax.Common |
setModalityArgInfo | Agda.Syntax.Common |
setModeUnlessInHardCompileTimeMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setModuleCheckpoint | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setMutual | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setMutualBlockInfo | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setNamedArg | Agda.Syntax.Common |
setNamedScope | Agda.Syntax.Scope.Monad |
setNameOf | Agda.Syntax.Common |
setNameSpace | Agda.Syntax.Scope.Base |
setNameSuffix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
setNotInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setOptionsFromPragma' | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setOrigin | Agda.Syntax.Common |
setOriginArgInfo | Agda.Syntax.Common |
setParsePos | Agda.Syntax.Parser.Monad |
setPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setPersistentVerbosity | Agda.Interaction.Options.Lenses |
setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
setPristineLock | Agda.Syntax.Concrete.Attribute |
setPristineQuantity | Agda.Syntax.Concrete.Attribute |
setPristineRelevance | Agda.Syntax.Concrete.Attribute |
setPtr | Agda.Utils.Pointer |
setQuantity | Agda.Syntax.Common |
setQuantityMod | Agda.Syntax.Common |
SetRange | |
1 (Type/Class) | Agda.Syntax.Position |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setRange | Agda.Syntax.Position |
setRelevance | Agda.Syntax.Common |
setRelevanceMod | Agda.Syntax.Common |
setRunTimeModeUnlessInHardCompileTimeMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SetS | Agda.Syntax.Reflected |
setSafeMode | Agda.Interaction.Options.Lenses |
setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setScopeAccess | Agda.Syntax.Scope.Base |
setScopeLocals | Agda.Syntax.Scope.Base |
setSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setSplitTree | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setTacticAttr | Agda.Syntax.Parser.Helpers |
setTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setTCLens' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SetToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
setToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setTreeless | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setUsability | Agda.Termination.Order |
setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
setVarsToBind | Agda.Syntax.Scope.Base |
setVerbosity | Agda.Interaction.Options.Lenses |
setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
several | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
SeveralConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SFalse | Agda.Utils.TypeLits |
sgListT | Agda.Utils.ListT |
sgMListT | Agda.Utils.ListT |
SgTel | Agda.Syntax.Internal |
sgTel | Agda.Syntax.Internal |
ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ShadowingInTelescope | |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
ShadowingInTelescope_ | Agda.Interaction.Options.Warnings |
shadowLocal | Agda.Syntax.Scope.Base |
Sharing | Agda.Utils.ProfileOptions |
sharing | Agda.Utils.Update |
shift | Agda.Compiler.JS.Substitution |
shifter | Agda.Compiler.JS.Substitution |
shiftFrom | Agda.Compiler.JS.Substitution |
ShouldAcceptAtLeastTwoArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
shouldBePath | Agda.TypeChecking.Telescope |
ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
shouldBePi | Agda.TypeChecking.Telescope |
shouldBePiOrPath | Agda.TypeChecking.Telescope |
shouldBeProjectible | Agda.TypeChecking.Records |
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 |
ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
shouldPostponeInstanceSearch | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.TypeChecking.InstanceArguments, Agda.Compiler.Backend |
shouldReduceDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
showA | Agda.Syntax.Abstract.Pretty |
showATop | Agda.Syntax.Abstract.Pretty |
showChar' | Agda.Syntax.Literal |
showComputed | Agda.Interaction.BasicOps |
showGeneralizedArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
showGoals | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop |
ShowHead | Agda.TypeChecking.Rules.Decl |
showHead | Agda.TypeChecking.Rules.Decl |
showIdentitySubstitutions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ShowImplicitArgs | Agda.Interaction.Base |
showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
showInfoError | Agda.Interaction.EmacsTop |
showIOException | Agda.Utils.IO |
ShowIrrelevantArgs | Agda.Interaction.Base |
showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
showModuleContents | Agda.Interaction.InteractionTop |
showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
showText | Agda.Syntax.Literal |
showThousandSep | Agda.Utils.String |
showUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SigAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SigCubicalNotErasure | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SigError | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sigError | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sigInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sigmaCon | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
sigmaFst | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
SigmaKit | |
1 (Type/Class) | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
2 (Data Constructor) | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
sigmaName | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
sigmaSnd | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SigUnknown | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
simpleBinaryOperator | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
simpleHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
simpleName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
Simplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Simplified | Agda.Interaction.Base |
Simplify | Agda.TypeChecking.Reduce |
simplify | Agda.TypeChecking.Reduce |
simplify1 | |
1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
simplifyBlocked' | Agda.TypeChecking.Reduce |
simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints |
simplifyTTerm | Agda.Compiler.Treeless.Simplify |
simplifyWithHypotheses | Agda.TypeChecking.SizedTypes.WarshallSolver |
SingleClosed | Agda.TypeChecking.Level |
singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SingleLevel | Agda.TypeChecking.Level |
SingleLevel' | Agda.TypeChecking.Level |
singleLevelView | Agda.TypeChecking.Level |
SinglePass | Agda.Compiler.ToTreeless |
SinglePlus | Agda.TypeChecking.Level |
Singleton | Agda.Utils.Singleton |
singleton | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.BoolSet |
3 (Function) | Agda.Utils.Bag |
4 (Function) | Agda.Utils.IntSet.Infinite |
5 (Function) | Agda.Utils.SmallSet |
6 (Function) | Agda.Utils.List1 |
7 (Function) | Agda.Utils.Singleton |
8 (Function) | Agda.Utils.Trie |
9 (Function) | Agda.Utils.BiMap |
10 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
11 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
singletonDT | Agda.TypeChecking.DiscrimTree.Types |
SingletonRecords | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
singletonS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
SingleVar | Agda.TypeChecking.Free.Lazy |
singPlural | Agda.Syntax.Common.Pretty |
Size | |
1 (Type/Class) | Agda.Termination.SparseMatrix |
2 (Data Constructor) | Agda.Termination.SparseMatrix |
size | |
1 (Function) | Agda.Utils.BoolSet |
2 (Function) | Agda.Utils.Bag |
3 (Function) | Agda.Utils.Size |
4 (Function) | Agda.Termination.SparseMatrix |
sizeBuiltins | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SizeConst | Agda.Utils.Warshall |
SizeConstraint | Agda.TypeChecking.SizedTypes.Syntax |
sizeConstraint | Agda.TypeChecking.SizedTypes.Syntax |
sizeContext | Agda.TypeChecking.SizedTypes.Syntax |
Sized | Agda.Utils.Size |
sizedText | Agda.Syntax.Common.Pretty |
SizedThing | |
1 (Type/Class) | Agda.Utils.Size |
2 (Data Constructor) | Agda.Utils.Size |
sizedThing | Agda.Utils.Size |
sizedTypesOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SizeExpr | |
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.Syntax |
sizeHypotheses | Agda.TypeChecking.SizedTypes.Syntax |
SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SizeLtSat | Agda.Interaction.Base |
sizeMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SizeMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sizeMaxView | Agda.TypeChecking.SizedTypes |
SizeMaxView' | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SizeMeta | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
3 (Data Constructor) | Agda.TypeChecking.SizedTypes |
sizeMetaArgs | Agda.TypeChecking.SizedTypes.Syntax |
sizeMetaId | Agda.TypeChecking.SizedTypes.Syntax |
SizeOfSort | |
1 (Type/Class) | Agda.TypeChecking.Substitute |
2 (Data Constructor) | Agda.TypeChecking.Substitute |
sizeOfSort | Agda.TypeChecking.Substitute |
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 | Agda.Compiler.Backend.Base, Agda.Compiler.Backend |
skip | Agda.Syntax.Parser.LexActions |
skipBlock | Agda.Syntax.Parser.Comments |
skipIrrelevantAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
SkipIrrelevantEquation | Agda.TypeChecking.Rules.LHS.Unify.Types |
SleepingConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
slowNormaliseArgs | Agda.TypeChecking.Reduce |
slowReduceTerm | Agda.TypeChecking.Reduce |
smallest | Agda.TypeChecking.SizedTypes.WarshallSolver |
SmallSet | |
1 (Type/Class) | Agda.Utils.SmallSet |
2 (Data Constructor) | Agda.Utils.SmallSet |
SmallSetElement | Agda.Utils.SmallSet |
SmallSort | Agda.TypeChecking.Substitute |
smashTel | Agda.Syntax.Concrete.Pretty |
snd3 | Agda.Utils.Tuple |
snoc | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.List1 |
Solution | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
3 (Type/Class) | Agda.Utils.Warshall |
4 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types |
solutionAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
solutionSide | Agda.TypeChecking.Rules.LHS.Unify.Types |
solutionTerm | Agda.TypeChecking.Rules.LHS.Unify.Types |
solutionType | Agda.TypeChecking.Rules.LHS.Unify.Types |
solutionVar | Agda.TypeChecking.Rules.LHS.Unify.Types |
solve | Agda.Utils.Warshall |
solveAwakeConstraints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solveAwakeConstraints' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solveAwakeInstanceConstraints | Agda.TypeChecking.InstanceArguments |
solveCluster | Agda.TypeChecking.SizedTypes.Solve |
solveConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solveConstraintTCM | Agda.TypeChecking.Constraints |
solveConstraint_ | Agda.TypeChecking.Constraints |
SolvedButOpenHoles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solvedMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solveEq | Agda.TypeChecking.Rules.LHS.Unify.Types |
solveGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
solveGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
solveInstantiatedGoals | Agda.Interaction.InteractionTop |
solveSizeConstraints | Agda.TypeChecking.SizedTypes.Solve |
solveSizeConstraints_ | Agda.TypeChecking.SizedTypes.Solve |
solveSomeAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solveSomeAwakeConstraintsTCM | Agda.TypeChecking.Constraints |
solveVar | Agda.TypeChecking.Rules.LHS.Unify.Types |
solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
solvingProblems | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Some | |
1 (Type/Class) | Agda.Utils.IndexedList |
2 (Data Constructor) | Agda.Utils.IndexedList |
some1 | Agda.Utils.List1 |
SomeBuiltin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
someBuiltin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SomeGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SomeKindsOfNames | Agda.Syntax.Scope.Base |
someKindsOfNames | Agda.Syntax.Scope.Base |
SomeWhere | Agda.Syntax.Concrete |
Sort | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Syntax.Reflected |
5 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
sort | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.TypeChecking.Substitute |
Sort' | Agda.Syntax.Internal |
sortBy | Agda.Utils.List1 |
SortCannotDependOnItsIndex | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortDefs | Agda.Compiler.Common |
SortDoesNotAdmitDataDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sorted | Agda.Utils.List |
sortFitsIn | Agda.TypeChecking.Sort |
SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortInteractionPoints | Agda.Interaction.InteractionTop |
SortIntervalUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortK | Agda.TypeChecking.DiscrimTree.Types |
SortKit | |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortLevelUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortOf | Agda.TypeChecking.Sort |
SortOfSplitVarError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortOfType | Agda.TypeChecking.Sort |
SortOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortOn | Agda.Utils.List1 |
SortProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortPropOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortRulesOfSymbol | Agda.TypeChecking.Rewriting.Confluence |
SortSet | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortSetOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortStrictSet | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortStrictSetOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SortUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
sortWith | Agda.Utils.List1 |
Source | |
1 (Type/Class) | Agda.Interaction.Imports |
2 (Data Constructor) | Agda.Interaction.Imports |
source | |
1 (Function) | Agda.Utils.BiMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph |
SourceFile | |
1 (Type/Class) | Agda.Interaction.FindFile |
2 (Data Constructor) | Agda.Interaction.FindFile |
sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
Space | Agda.Compiler.JS.Pretty |
space | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.Compiler.JS.Pretty |
Span | |
1 (Type/Class) | Agda.Syntax.Common.Pretty |
2 (Data Constructor) | Agda.Syntax.Common.Pretty |
span | Agda.Utils.List1 |
spanAllowedBeforeModule | Agda.Syntax.Concrete |
spanAnnotation | Agda.Syntax.Common.Pretty |
spanEnd | Agda.Utils.List |
spanJust | Agda.Utils.List |
spanLength | Agda.Syntax.Common.Pretty |
spanMaybe | Agda.Utils.Maybe |
spanStart | Agda.Syntax.Common.Pretty |
SpecialCharacters | |
1 (Type/Class) | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
2 (Data Constructor) | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
specialCharactersForGlyphs | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
Specified | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
spLhsDefName | Agda.Syntax.Abstract |
spLhsInfo | Agda.Syntax.Abstract |
spLhsPats | Agda.Syntax.Abstract |
splitApplyElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
splitArg | Agda.TypeChecking.Coverage.SplitTree |
SplitAt | Agda.TypeChecking.Coverage.SplitTree |
splitAt | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.RangeMap |
splitBindings | Agda.TypeChecking.Coverage.SplitTree |
splitC | Agda.TypeChecking.CompiledClause.Compile |
SplitCatchall | Agda.TypeChecking.Coverage.SplitTree |
SplitClause | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
splitClauses | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
splitClauseWithAbsurd | Agda.TypeChecking.Coverage |
splitCommas | Agda.Interaction.Library.Parse |
SplitCon | Agda.TypeChecking.Coverage.SplitTree |
splitEllipsis | Agda.Syntax.Concrete.Pattern |
SplitError | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
splitExactlyAt | Agda.Utils.List |
splitExcludedLits | Agda.TypeChecking.Coverage.Match |
SplitInProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
splitLast | Agda.TypeChecking.Coverage |
splitLazy | Agda.TypeChecking.Coverage.SplitTree |
SplitLit | Agda.TypeChecking.Coverage.SplitTree |
splitOffTrailingWithPatterns | Agda.Syntax.Abstract.Pattern |
splitOn | Agda.TypeChecking.CompiledClause.Compile |
SplitOnAbstract | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitOnCoinductive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitOnFlat | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify |
SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitOnNonEtaRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitOnNonVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitOnPartial | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitOnStrict | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify |
SplitOnUnchecked | 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.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
SplitTag | Agda.TypeChecking.Coverage.SplitTree |
SplitTel | |
1 (Type/Class) | Agda.TypeChecking.Telescope |
2 (Data Constructor) | Agda.TypeChecking.Telescope |
splitTelescope | Agda.TypeChecking.Telescope |
splitTelescopeAt | Agda.TypeChecking.Telescope |
splitTelescopeExact | Agda.TypeChecking.Telescope |
splitTelForWith | Agda.TypeChecking.With |
SplittingDone | Agda.TypeChecking.Coverage.SplitTree |
SplitTree | Agda.TypeChecking.Coverage.SplitTree |
SplitTree' | Agda.TypeChecking.Coverage.SplitTree |
SplitTreeLabel | |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree |
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree |
SplitTrees | Agda.TypeChecking.Coverage.SplitTree |
splitTrees | Agda.TypeChecking.Coverage.SplitTree |
SplitTrees' | Agda.TypeChecking.Coverage.SplitTree |
square | Agda.Termination.SparseMatrix |
Squash | Agda.Syntax.Common |
src | Agda.TypeChecking.SizedTypes.WarshallSolver |
srcAttributes | Agda.Interaction.Imports |
SrcFile | Agda.Syntax.Position |
srcFile | Agda.Syntax.Position |
srcFilePath | Agda.Interaction.FindFile |
srcFileType | Agda.Interaction.Imports |
SrcFun | Agda.Utils.CallStack |
SrcLoc | |
1 (Data Constructor) | Agda.Utils.CallStack |
2 (Type/Class) | Agda.Utils.CallStack |
SrcLocCol | Agda.Utils.CallStack |
srcLocEndCol | Agda.Utils.CallStack |
srcLocEndLine | Agda.Utils.CallStack |
SrcLocFile | Agda.Utils.CallStack |
srcLocFile | Agda.Utils.CallStack |
SrcLocLine | Agda.Utils.CallStack |
SrcLocModule | Agda.Utils.CallStack |
srcLocModule | Agda.Utils.CallStack |
SrcLocPackage | Agda.Utils.CallStack |
srcLocPackage | Agda.Utils.CallStack |
srcLocStartCol | Agda.Utils.CallStack |
srcLocStartLine | Agda.Utils.CallStack |
srcModule | Agda.Interaction.Imports |
srcModuleName | Agda.Interaction.Imports |
srcNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
srcOrigin | Agda.Interaction.Imports |
srcProjectLibs | Agda.Interaction.Imports |
srcText | Agda.Interaction.Imports |
SSet | Agda.Syntax.Internal |
sShowImplicitArguments | Agda.Interaction.Response.Base, Agda.Interaction.Response |
sShowIrrelevantArguments | Agda.Interaction.Response.Base, Agda.Interaction.Response |
sSizeUniv | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
ssort | Agda.TypeChecking.Substitute |
SSSMismatch | Agda.Utils.List |
SSSResult | Agda.Utils.List |
SSSStrip | Agda.Utils.List |
St | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
2 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
stAccumStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Stack | Agda.TypeChecking.CompiledClause.Match |
stAgdaLibFiles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
standardOptions | Agda.Interaction.Options |
standardOptions_ | Agda.Interaction.Options |
stAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
starP | Agda.Utils.Parser.MemoisedCPS |
StarSemiRing | Agda.Utils.SemiRing |
startPos | Agda.Syntax.Position |
startPos' | Agda.Syntax.Position |
stateTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stateTCLensM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
StaticPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Statistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stats | Agda.TypeChecking.Serialise.Base |
Status | |
1 (Type/Class) | Agda.Interaction.Response.Base, Agda.Interaction.Response |
2 (Data Constructor) | Agda.Interaction.Response.Base, Agda.Interaction.Response |
status | Agda.Interaction.InteractionTop |
stAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stCopiedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
StdErr | Agda.TypeChecking.Unquote |
StdIn | Agda.TypeChecking.Unquote |
stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
StdOut | Agda.TypeChecking.Unquote |
stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stealConstraintsTCM | Agda.TypeChecking.Constraints |
sTextC | Agda.TypeChecking.Serialise.Base |
sTextD | Agda.TypeChecking.Serialise.Base |
sTextE | Agda.TypeChecking.Serialise.Base |
stForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshOpaqueId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stImportedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
stInstanceTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stInstantiateBlocking | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stLocalPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Stmt | Agda.Utils.Haskell.Syntax |
stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stNameCopies | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stOpenMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
storeCachedAgdaLibFile | Agda.Interaction.Library.Base |
storeCachedProjectConfig | Agda.Interaction.Library.Base |
storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
storeDisambiguatedConstructor | Agda.Interaction.Highlighting.Generate |
storeDisambiguatedProjection | Agda.Interaction.Highlighting.Generate |
stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
stPersistentTopLevelModuleNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPersistLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshOpaqueId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostInstantiateBlocking | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostLocalPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostOpenMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostPendingInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostponeInstanceSearch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostPostponeInstanceSearch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostSolvedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostTCWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostTemporaryInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPostUsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreAgdaLibFiles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreCopiedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreImportedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
stPreNameCopies | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPrePatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPrePatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPrePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stPreProjectConfigs | 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 |
stProjectConfigs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Strengthen | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
strengthen | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
strengthenS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
strengthenS' | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
Strict | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Type/Class) | Agda.Utils.Maybe.Strict |
strictCurry | Agda.Utils.TypeLevel |
StrictCurrying | Agda.Utils.TypeLevel |
strictCurrys | Agda.Utils.TypeLevel |
Strictness | Agda.Utils.Haskell.Syntax |
StrictPair | Agda.Utils.TypeLevel |
StrictPos | Agda.TypeChecking.Positivity.Occurrence |
StrictProducts | Agda.Utils.TypeLevel |
StrictSplit | Agda.TypeChecking.Coverage.SplitTree |
strictUncurry | Agda.Utils.TypeLevel |
strictUncurrys | Agda.Utils.TypeLevel |
String | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
3 (Data Constructor) | Agda.Compiler.JS.Syntax |
4 (Data Constructor) | Agda.Interaction.JSON |
String1 | Agda.Utils.List1 |
string2HelpTopic | Agda.Interaction.Options.Help |
string2WarningName | Agda.Interaction.Options.Warnings |
stringC | Agda.TypeChecking.Serialise.Base |
stringD | Agda.TypeChecking.Serialise.Base |
stringE | Agda.TypeChecking.Serialise.Base |
stringNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
stringParts | Agda.Syntax.Notation |
stringTCErr | Agda.TypeChecking.Errors |
stringToArgName | Agda.Syntax.Common |
stringToAttribute | Agda.Syntax.Concrete.Attribute |
stringToRawName | Agda.Syntax.Common |
stripArgLeft | Agda.TypeChecking.Rules.LHS.Unify.Types |
stripArgRight | Agda.TypeChecking.Rules.LHS.Unify.Types |
stripAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
stripConstraintPids | Agda.Interaction.BasicOps |
stripDontCare | Agda.Syntax.Internal |
stripNoNames | Agda.Syntax.Scope.Monad |
stripPrefixBy | Agda.Utils.List |
stripReversedSuffix | Agda.Utils.List |
stripRTS | Agda.Interaction.Options |
StripSizeSuc | Agda.TypeChecking.Rules.LHS.Unify.Types |
stripSuffix | Agda.Utils.List |
stripUnusedArguments | Agda.Compiler.Treeless.Unused |
stripWithClausePatterns | Agda.TypeChecking.With |
strongly | Agda.TypeChecking.MetaVars.Occurs |
StronglyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
stronglyRigidVars | Agda.TypeChecking.Free |
StrPart | Agda.TypeChecking.Unquote |
StrSufSt | Agda.Utils.List |
STrue | Agda.Utils.TypeLits |
stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stSolvedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stTCWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stTemporaryInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stTopLevelModuleNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
StuckOn | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
stuckOn | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
stUsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
stWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Style | |
1 (Type/Class) | Agda.Syntax.Common.Pretty |
2 (Data Constructor) | Agda.Syntax.Common.Pretty |
style | Agda.Syntax.Common.Pretty |
Sub | Agda.TypeChecking.Rewriting.NonLinMatch |
subLevel | Agda.TypeChecking.Level |
Subscript | Agda.Utils.Suffix |
Subst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
subst | |
1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Function) | Agda.Compiler.JS.Substitution |
3 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
subst' | Agda.Compiler.JS.Substitution |
SubstArg | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute, Agda.TypeChecking.Substitute |
substBody | Agda.TypeChecking.CompiledClause.Compile |
SubstCand | Agda.TypeChecking.MetaVars |
SubstExpr | Agda.Syntax.Abstract |
substExpr | Agda.Syntax.Abstract |
Substitute | Agda.TypeChecking.SizedTypes.Syntax |
substituter | Agda.Compiler.JS.Substitution |
Substitution | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
Substitution' | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
substPattern | Agda.Syntax.Abstract.Pattern |
substPattern' | Agda.Syntax.Abstract.Pattern |
substUnder | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
SubstWith | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
subtract | Agda.Utils.VarSet |
subtypingForSizeLt | Agda.TypeChecking.MetaVars |
subVar | Agda.TypeChecking.Free.Lazy |
Suc | Agda.Utils.IndexedList |
Succ | Agda.Utils.Size |
sucName | Agda.TypeChecking.Level |
Suffix | |
1 (Type/Class) | Agda.Utils.Suffix |
2 (Type/Class) | Agda.Utils.List |
3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
suffixesSatisfying | Agda.Utils.List |
suffixNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
suffixToLevel | Agda.TypeChecking.Rules.Application |
suffixView | Agda.Utils.Suffix |
Suggest | Agda.Syntax.Internal |
Suggestion | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
suggestName | Agda.Syntax.Internal |
suggests | Agda.Syntax.Internal |
SumEncoding | Agda.Interaction.JSON |
sumEncoding | Agda.Interaction.JSON |
superscript | Agda.TypeChecking.Pretty |
supremum | Agda.Termination.Order |
supSize | Agda.Termination.SparseMatrix |
swap | Agda.Utils.Tuple |
swap01 | Agda.TypeChecking.Abstract |
swapEither | Agda.Utils.Either |
switchBenchmarking | Agda.Utils.Benchmark |
SymArrow | Agda.Syntax.Parser.Tokens |
SymAs | Agda.Syntax.Parser.Tokens |
SymBar | Agda.Syntax.Parser.Tokens |
Symbol | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
3 (Type/Class) | Agda.Syntax.Parser.Tokens |
symbol | Agda.Syntax.Parser.LexActions |
SymCloseBrace | Agda.Syntax.Parser.Tokens |
SymCloseIdiomBracket | Agda.Syntax.Parser.Tokens |
SymCloseParen | Agda.Syntax.Parser.Tokens |
SymClosePragma | Agda.Syntax.Parser.Tokens |
SymCloseVirtualBrace | Agda.Syntax.Parser.Tokens |
SymColon | Agda.Syntax.Parser.Tokens |
SymDot | Agda.Syntax.Parser.Tokens |
SymDotDot | Agda.Syntax.Parser.Tokens |
SymDoubleCloseBrace | Agda.Syntax.Parser.Tokens |
SymDoubleOpenBrace | Agda.Syntax.Parser.Tokens |
SymEllipsis | Agda.Syntax.Parser.Tokens |
SymEmptyIdiomBracket | Agda.Syntax.Parser.Tokens |
SymEndComment | Agda.Syntax.Parser.Tokens |
SymEqual | Agda.Syntax.Parser.Tokens |
SymLambda | Agda.Syntax.Parser.Tokens |
SymOpenBrace | Agda.Syntax.Parser.Tokens |
SymOpenIdiomBracket | Agda.Syntax.Parser.Tokens |
SymOpenParen | Agda.Syntax.Parser.Tokens |
SymOpenPragma | Agda.Syntax.Parser.Tokens |
SymOpenVirtualBrace | Agda.Syntax.Parser.Tokens |
SymQuestionMark | Agda.Syntax.Parser.Tokens |
SymSemi | Agda.Syntax.Parser.Tokens |
SymUnderscore | Agda.Syntax.Parser.Tokens |
SymVirtualSemi | Agda.Syntax.Parser.Tokens |
sync | Agda.Syntax.Parser.LookAhead |
SynEq | Agda.TypeChecking.SyntacticEquality |
syntacticEqualityFuelRemains | Agda.TypeChecking.SyntacticEquality |
Syntax | Agda.Syntax.Concrete |
SyntaxBindingLambda | Agda.Syntax.Concrete |
syntaxOf | Agda.Syntax.Notation |
System | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
systemClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
systemTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
szSortSize | Agda.TypeChecking.Substitute |
szSortUniv | Agda.TypeChecking.Substitute |