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

Index - W

waitokAgda.Auto.NarrowingSearch
wakeConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
wakeConstraints'Agda.TypeChecking.Constraints
wakeConstraintsTCMAgda.TypeChecking.Constraints
wakeIfBlockedOnMetaAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnProblemAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIrrelevantVarsAgda.TypeChecking.Irrelevance
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.MetaVars
wakeUpWhenAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeUpWhen_Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
walkSatisfyingAgda.Utils.Graph.AdjacencyMap.Unidirectional
warn2ErrorAgda.Interaction.Options.Warnings
WarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
warningName2StringAgda.Interaction.Options.Warnings
WarningOnImportAgda.Syntax.Concrete
WarningOnUsageAgda.Syntax.Concrete
warnings 
1 (Function)Agda.Interaction.Library.Base
2 (Function)Agda.TypeChecking.Warnings
warnings'Agda.Interaction.Library.Base
WarningsAndNonFatalErrorsAgda.TypeChecking.Warnings, Agda.Interaction.Response
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
WeakAgda.Auto.Syntax
weakAgda.Auto.Syntax
weak'Agda.Auto.Syntax
WeakeningAgda.Auto.Syntax
weaklyAgda.TypeChecking.MetaVars.Occurs
WeaklyRigidAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
Weight 
1 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Type/Class)Agda.Utils.Warshall
wfAfterTelAgda.TypeChecking.Rules.Def
wfBeforeTelAgda.TypeChecking.Rules.Def
wfCallSubstAgda.TypeChecking.Rules.Def
wfClausesAgda.TypeChecking.Rules.Def
wfExprsAgda.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
whatInductionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
whenAgda.Utils.Monad
whenAbstractFreezeMetasAfterAgda.TypeChecking.Rules.Decl
whenConstraintsAgda.TypeChecking.Constraints
whenExactVerbosityAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
WhereAgda.TypeChecking.Positivity.Occurrence
WhereClauseAgda.Syntax.Concrete
WhereClause'Agda.Syntax.Concrete
WhereDeclarationsAgda.Syntax.Abstract
WhereDeclsAgda.Syntax.Abstract
whereDeclsAgda.Syntax.Abstract
whereModuleAgda.Syntax.Abstract
whHidingAgda.Syntax.Common
WhichWarningsAgda.TypeChecking.Warnings
whileLeftAgda.Utils.Either
whThingAgda.Syntax.Common
WhyInScopeAgda.Syntax.Scope.Base
whyInScope 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.InteractionTop
WildHoleAgda.Syntax.Common
WildP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
WildVAgda.Syntax.Concrete.Operators.Parser
WithAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
withAnonymousModuleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
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.Compiler.Backend, Agda.TypeChecking.Monad
withClosureAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
withCompilerFlagAgda.Compiler.MAlonzo.Compiler
withConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
withContextPrecedenceAgda.Syntax.Scope.Monad
withCoverageCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
withCurrentCallStackAgda.Utils.CallStack
withCurrentFileAgda.Interaction.InteractionTop
withCurrentModule 
1 (Function)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
2 (Function)Agda.Syntax.Scope.Monad
withCurrentModule'Agda.Syntax.Scope.Monad
WithDefaultAgda.Utils.WithDefault
withDisplayFormAgda.TypeChecking.With
withEmbeddedJSONAgda.Interaction.JSON
withEnvAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
withFreshName_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
withImportPathAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
withInteractionIdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
withIntervalAgda.Syntax.Parser.LexActions
withInterval'Agda.Syntax.Parser.LexActions
withInterval_Agda.Syntax.Parser.LexActions
WithKAgda.Syntax.Common
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
withMetaInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
withMetaInfo'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad
WithOrigin 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
withoutCacheAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
WithoutForceAgda.Interaction.Base
WithoutKAgda.Syntax.Common
WithoutKFlagPrimEraseEqualityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WithoutKFlagPrimEraseEquality_Agda.Interaction.Options.Warnings
withoutKOptionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Reduce
WithRHSAgda.Syntax.Abstract
withScientificAgda.Interaction.JSON
withScope 
1 (Function)Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Function)Agda.Syntax.Translation.AbstractToConcrete
withScope_Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WithSeenUIds 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
withShadowingNameTCMAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
withShowAllArgumentsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withShowAllArguments'Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withSignatureAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withSomeAgda.Utils.IndexedList
withTCStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withTerminationCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
withTextAgda.Interaction.JSON
withTopLevelModuleAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.List
workOnTypesAgda.TypeChecking.Irrelevance
workOnTypes'Agda.TypeChecking.Irrelevance
woThingAgda.Syntax.Common
writeFileAgda.Utils.IO.UTF8
writeIORefAgda.Utils.IORef
writeModule 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
writeTextToFileAgda.Utils.IO.UTF8
writeToCurrentLogAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
writeToTempFileAgda.Utils.IO.TempFile
WrongCohesionInLambdaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongContentBlockAgda.Syntax.Concrete.Definitions.Errors
WrongDefinitionAgda.Syntax.Concrete.Definitions.Errors
WrongHidingInApplicationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongHidingInLambdaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongHidingInLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongInstanceDeclarationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongInstanceDeclaration_Agda.Interaction.Options.Warnings
WrongIrrelevanceInLambdaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongModalityForPrimitiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongNamedArgumentAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongNumberOfConstructorArgumentsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongQuantityInLambdaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WSMAgda.Syntax.Scope.Monad