Agda-2.6.20240714: A dependently typed functional programming language and proof assistant

Index - W

wakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraints'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraintsTCMAgda.TypeChecking.Constraints
wakeIfBlockedOnDefAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnMetaAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnProblemAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIrrelevantVarsAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WakeUp 
1 (Type/Class)Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeupConstraintsAgda.TypeChecking.Constraints
wakeupConstraints_Agda.TypeChecking.Constraints
wakeupListenerAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeUpWhenAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeUpWhen_Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
walkSatisfyingAgda.Utils.Graph.AdjacencyMap.Unidirectional
warn2ErrorAgda.Interaction.Options.Warnings
warnForPlentyInHardCompileTimeModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningAgda.TypeChecking.Warnings
warning'Agda.TypeChecking.Warnings
warning'_Agda.TypeChecking.Warnings
warningHighlightingAgda.Interaction.Highlighting.Generate
WarningMode 
1 (Type/Class)Agda.Interaction.Options.Warnings, Agda.Interaction.Options
2 (Data Constructor)Agda.Interaction.Options.Warnings, Agda.Interaction.Options
WarningModeErrorAgda.Interaction.Options.Warnings
warningModeUpdateAgda.Interaction.Options.Warnings
WarningNameAgda.Interaction.Options.Warnings
warningNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningName2StringAgda.Interaction.Options.Warnings
WarningOnImportAgda.Syntax.Concrete
WarningOnUsageAgda.Syntax.Concrete
WarningProblemAgda.Interaction.Options
WarningProblem_Agda.Interaction.Options.Warnings
warnings 
1 (Function)Agda.Interaction.Library.Base
2 (Function)Agda.TypeChecking.Warnings
warnings'Agda.Interaction.Library.Base
WarningsAndNonFatalErrors 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Warnings, Agda.Interaction.Response, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningSetAgda.Interaction.Options.Warnings
warningSetsAgda.Interaction.Options.Warnings
warning_Agda.TypeChecking.Warnings
warnOnRecordFieldWarningsAgda.TypeChecking.Records
warnPolarityPragmasButNotPostulatesAgda.Syntax.Concrete.Fixity
warnRangeAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
warnUnknownFixityInMixfixDeclAgda.Syntax.Concrete.Fixity
warnUnknownNamesInFixityDeclAgda.Syntax.Concrete.Fixity
warnUnknownNamesInPolarityPragmasAgda.Syntax.Concrete.Fixity
warshallAgda.Utils.Warshall
warshallGAgda.Utils.Warshall
weaklyAgda.TypeChecking.MetaVars.Occurs
WeaklyRigidAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
Weight 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
wfAfterTelAgda.TypeChecking.Rules.Def
wfBeforeTelAgda.TypeChecking.Rules.Def
wfCallSubstAgda.TypeChecking.Rules.Def
wfClausesAgda.TypeChecking.Rules.Def
wfExprsAgda.TypeChecking.Rules.Def
wfLetBindingsAgda.TypeChecking.Rules.Def
wfNameAgda.TypeChecking.Rules.Def
wfParentNameAgda.TypeChecking.Rules.Def
wfParentParamsAgda.TypeChecking.Rules.Def
wfParentPatsAgda.TypeChecking.Rules.Def
wfParentTelAgda.TypeChecking.Rules.Def
wfParentTypeAgda.TypeChecking.Rules.Def
wfPermFinalAgda.TypeChecking.Rules.Def
wfPermParentAgda.TypeChecking.Rules.Def
wfPermSplitAgda.TypeChecking.Rules.Def
wfRHSTypeAgda.TypeChecking.Rules.Def
whenAgda.Utils.Monad
whenAbstractFreezeMetasAfterAgda.TypeChecking.Rules.Decl
whenConstraintsAgda.TypeChecking.Constraints
whenExactVerbosityAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
whenJust 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
whenJustM 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
whenMAgda.Utils.Monad
whenNothingAgda.Utils.Maybe
whenNothingMAgda.Utils.Maybe
whenNullAgda.Utils.Null
whenNullMAgda.Utils.Null
whenProfileAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhereAgda.TypeChecking.Positivity.Occurrence
whereAnywhereAgda.Syntax.Abstract
WhereClauseAgda.Syntax.Concrete
WhereClause'Agda.Syntax.Concrete
WhereDeclarationsAgda.Syntax.Abstract
WhereDeclarationsSpineAgda.Syntax.Abstract
whereDeclarationsSpineAgda.Syntax.Abstract
WhereDeclsAgda.Syntax.Abstract
whereDeclsAgda.Syntax.Abstract
WhereDeclsSAgda.Syntax.Abstract
whereModuleAgda.Syntax.Abstract
whHidingAgda.Syntax.Common
WhichWarningsAgda.TypeChecking.Warnings
whileLeftAgda.Utils.Either
whThingAgda.Syntax.Common
WhyCheckModalityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhyInScopeAgda.Syntax.Scope.Base
whyInScope 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.InteractionTop
WhyInScopeData 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
whyInScopeDataFromAmbiguousNameReasonAgda.Syntax.Scope.Base
WildP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
WildPartAgda.Syntax.Common
WildVAgda.Syntax.Concrete.Operators.Parser
WithAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
withAnonymousModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
withAppBracketsAgda.Syntax.Fixity
WithArgCtxAgda.Syntax.Fixity
withArgsFromAgda.Syntax.Common
withArgumentsAgda.TypeChecking.With
WithArity 
1 (Type/Class)Agda.TypeChecking.CompiledClause
2 (Data Constructor)Agda.TypeChecking.CompiledClause
withArrayAgda.Interaction.JSON
withBoolAgda.Interaction.JSON
WithBoundAgda.Syntax.Scope.Base
withCallerCallStackAgda.Utils.CallStack
withCatchallPragmaAgda.Syntax.Concrete.Definitions.Monad
withCheckNoShadowingAgda.Syntax.Scope.Monad
WithClausePatternMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withClosureAgda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withContextPrecedenceAgda.Syntax.Scope.Monad
withCoverageCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
withCurrentCallStackAgda.Utils.CallStack
withCurrentFileAgda.Interaction.InteractionTop
withCurrentModule 
1 (Function)Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.Syntax.Scope.Monad
withCurrentModule'Agda.Syntax.Scope.Monad
WithDefaultAgda.Utils.WithDefault
WithDefault'Agda.Utils.WithDefault
withDisplayFormAgda.TypeChecking.With
withEmbeddedJSONAgda.Interaction.JSON
withEnvAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithExpr 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
WithExpr'Agda.Syntax.Abstract
withExtendedOccEnvAgda.TypeChecking.Positivity
withExtendedOccEnv'Agda.TypeChecking.Positivity
WithForceAgda.Interaction.Base
withFreshNameAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFreshName_Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFrozenMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithFunctionAgda.TypeChecking.Rules.Def
WithFunctionProblemAgda.TypeChecking.Rules.Def
withFunctionTypeAgda.TypeChecking.With
WithFunCtxAgda.Syntax.Fixity
WithHiding 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
withHidingAgda.Syntax.Concrete.Pretty
withHighlightingLevelAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withImportPathAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withInteractionIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withIntervalAgda.Syntax.Parser.LexActions
withInterval'Agda.Syntax.Parser.LexActions
withInterval_Agda.Syntax.Parser.LexActions
WithKAgda.Syntax.Common
WithKEnabledAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
WithKind 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
withLayoutAgda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVarsAgda.Syntax.Scope.Monad
withMetaIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withMetaInfo'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withNameAgda.Syntax.Translation.ReflectedToAbstract
withNamedArgsFromAgda.Syntax.Common
withNamesAgda.Syntax.Translation.ReflectedToAbstract
withNBackCallStackAgda.Utils.CallStack
WithNode 
1 (Type/Class)Agda.TypeChecking.Pretty
2 (Data Constructor)Agda.TypeChecking.Pretty
withObjectAgda.Interaction.JSON
WithOnFreeVariableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithOrigin 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
withoutCacheAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithoutForceAgda.Interaction.Base
WithoutKAgda.Syntax.Common
WithoutKFlagPrimEraseEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithoutKFlagPrimEraseEquality_Agda.Interaction.Options.Warnings
withoutKOptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutPrintingGeneralizationAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutPrivatesAgda.Syntax.Scope.Base
WithP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
withPositivityCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
withPragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withRangeOfAgda.Syntax.Position
withRangesOfAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
withRangesOfQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
withReducedAgda.TypeChecking.Constraints
WithRHSAgda.Syntax.Abstract
WithRHSSAgda.Syntax.Abstract
withScientificAgda.Interaction.JSON
withScope 
1 (Function)Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.Syntax.Translation.AbstractToConcrete
withScope_Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShadowingNameTCMAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShowAllArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShowAllArguments'Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withSignatureAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withSomeAgda.Utils.IndexedList
withTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withTerminationCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
withTextAgda.Interaction.JSON
withTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithUniqueInt 
1 (Type/Class)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Data Constructor)Agda.Utils.Graph.AdjacencyMap.Unidirectional
withUniverseCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
withUsableVarsAgda.Termination.Monad
withVarAgda.Syntax.Translation.ReflectedToAbstract
withVarOccAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
withVarsAgda.Syntax.Translation.ReflectedToAbstract
WkAgda.Syntax.Internal, Agda.TypeChecking.Substitute
wkSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
woOriginAgda.Syntax.Common
word64ViewAgda.Syntax.Treeless, Agda.Compiler.Backend
wordBoundedAgda.Interaction.Highlighting.Vim
wordsByAgda.Utils.List1
workOnTypesAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
workOnTypes'Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
woThingAgda.Syntax.Common
writeFileAgda.Utils.IO.UTF8
writeIORefAgda.Utils.IORef
writeModuleAgda.Compiler.JS.Compiler
writeTextToFileAgda.Utils.IO.UTF8
writeToCurrentLogAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
writeToTempFileAgda.Utils.IO.TempFile
writeUnifyLogAgda.TypeChecking.Rules.LHS.Unify.Types
WrongArgInfoForPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongCohesionInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongContentBlockAgda.Syntax.Concrete.Definitions.Errors
WrongDefinitionAgda.Syntax.Concrete.Definitions.Errors
WrongHidingInApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongInstanceDeclarationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongInstanceDeclaration_Agda.Interaction.Options.Warnings
WrongIrrelevanceInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNamedArgumentAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNumberOfConstructorArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongQuantityInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WSMAgda.Syntax.Scope.Monad