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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - W

wakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraints' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraintsTCM | Agda.TypeChecking.Constraints
wakeIfBlockedOnDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIrrelevantVars | Agda.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
wakeupConstraints | Agda.TypeChecking.Constraints
wakeupConstraints_ | Agda.TypeChecking.Constraints
wakeupListener | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeUpWhen | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeUpWhen_ | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
walkSatisfying | Agda.Utils.Graph.AdjacencyMap.Unidirectional
warn2Error | Agda.Interaction.Options.Warnings
warnEmptyPolarityPragma | Agda.Syntax.Concrete.Fixity
warnForPlentyInHardCompileTimeMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Warning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warning | Agda.TypeChecking.Warnings
warning' | Agda.TypeChecking.Warnings
warning'_ | Agda.TypeChecking.Warnings
warningHighlighting | Agda.Interaction.Highlighting.Generate
WarningMode |
1 (Type/Class) | Agda.Interaction.Options.Warnings, Agda.Interaction.Options
2 (Data Constructor) | Agda.Interaction.Options.Warnings, Agda.Interaction.Options
WarningModeError | Agda.Interaction.Options.Warnings
warningModeUpdate | Agda.Interaction.Options.Warnings
WarningName | Agda.Interaction.Options.Warnings
warningName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningName2String | Agda.Interaction.Options.Warnings
WarningOnImport | Agda.Syntax.Concrete
WarningOnUsage | Agda.Syntax.Concrete
WarningProblem | Agda.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
warningSet | Agda.Interaction.Options.Warnings
warningSets | Agda.Interaction.Options.Warnings
warning_ | Agda.TypeChecking.Warnings
warnOnRecordFieldWarnings | Agda.TypeChecking.Records
warnPolarityPragmasButNotPostulates | Agda.Syntax.Concrete.Fixity
warnRange | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
warnUnknownFixityInMixfixDecl | Agda.Syntax.Concrete.Fixity
warnUnknownNamesInFixityDecl | Agda.Syntax.Concrete.Fixity
warnUnknownNamesInPolarityPragmas | Agda.Syntax.Concrete.Fixity
weakly | Agda.TypeChecking.MetaVars.Occurs
WeaklyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
Weight | Agda.TypeChecking.SizedTypes.WarshallSolver
wfAfterTel | Agda.TypeChecking.Rules.Def
wfBeforeTel | Agda.TypeChecking.Rules.Def
wfCallSubst | Agda.TypeChecking.Rules.Def
wfClauses | Agda.TypeChecking.Rules.Def
wfExprs | Agda.TypeChecking.Rules.Def
wfLetBindings | Agda.TypeChecking.Rules.Def
wfName | Agda.TypeChecking.Rules.Def
wfParentName | Agda.TypeChecking.Rules.Def
wfParentParams | Agda.TypeChecking.Rules.Def
wfParentPats | Agda.TypeChecking.Rules.Def
wfParentTel | Agda.TypeChecking.Rules.Def
wfParentType | Agda.TypeChecking.Rules.Def
wfPermFinal | Agda.TypeChecking.Rules.Def
wfPermParent | Agda.TypeChecking.Rules.Def
wfPermSplit | Agda.TypeChecking.Rules.Def
wfRHSType | Agda.TypeChecking.Rules.Def
when | Agda.Utils.Monad
whenAbstractFreezeMetasAfter | Agda.TypeChecking.Rules.Decl
whenConstraints | Agda.TypeChecking.Constraints
whenExactVerbosity | Agda.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
whenM | Agda.Utils.Monad
whenNothing | Agda.Utils.Maybe
whenNothingM | Agda.Utils.Maybe
whenNull | Agda.Utils.Null
whenNullM | Agda.Utils.Null
whenProfile | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Where | Agda.TypeChecking.Positivity.Occurrence
whereAnywhere | Agda.Syntax.Abstract
WhereClause | Agda.Syntax.Concrete
WhereClause' | Agda.Syntax.Concrete
WhereClausesNotAllowed | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhereClause_ | Agda.Syntax.Concrete
whereClause_ | Agda.Syntax.Concrete
WhereDeclarations | Agda.Syntax.Abstract
WhereDeclarationsSpine | Agda.Syntax.Abstract
whereDeclarationsSpine | Agda.Syntax.Abstract
WhereDecls | Agda.Syntax.Abstract
whereDecls | Agda.Syntax.Abstract
WhereDeclsS | Agda.Syntax.Abstract
whereModule | Agda.Syntax.Abstract
whHiding | Agda.Syntax.Common
WhichWarnings | Agda.TypeChecking.Warnings
whileLeft | Agda.Utils.Either
whThing | Agda.Syntax.Common
WhyCheckModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhyInScope | Agda.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
whyInScopeDataFromAmbiguousNameReason | Agda.Syntax.Scope.Base
WhyInvalidInstanceType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhyNotAHaskellType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WildP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
WildPart | Agda.Syntax.Common
WildV | Agda.Syntax.Concrete.Operators.Parser
With | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
withAnonymousModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithApp |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
withAppBrackets | Agda.Syntax.Fixity
WithArgCtx | Agda.Syntax.Fixity
withArgsFrom | Agda.Syntax.Common
withArguments | Agda.TypeChecking.With
WithArity |
1 (Type/Class) | Agda.TypeChecking.CompiledClause
2 (Data Constructor) | Agda.TypeChecking.CompiledClause
withArray | Agda.Interaction.JSON
withBool | Agda.Interaction.JSON
WithBound | Agda.Syntax.Scope.Base
withCallerCallStack | Agda.Utils.CallStack
withCatchallPragma | Agda.Syntax.Concrete.Definitions.Monad
withCheckNoShadowing | Agda.Syntax.Scope.Monad
withClausePattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithClausePatternMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithClausePatternMismatch_ | Agda.Interaction.Options.Errors
WithClauseProjectionFixityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithClauseProjectionFixityMismatch_ | Agda.Interaction.Options.Warnings
withClauseProjectionOrigin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withContextPrecedence | Agda.Syntax.Scope.Monad
withCoverageCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
withCurrentCallStack | Agda.Utils.CallStack
withCurrentFile | Agda.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
WithDefault | Agda.Utils.WithDefault
WithDefault' | Agda.Utils.WithDefault
withDisplayForm | Agda.TypeChecking.With
withEmbeddedJSON | Agda.Interaction.JSON
withEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withError | Agda.Utils.Monad
WithExpr |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
WithExpr' | Agda.Syntax.Abstract
withExtendedOccEnv | Agda.TypeChecking.Positivity
withExtendedOccEnv' | Agda.TypeChecking.Positivity
WithForce | Agda.Interaction.Base
withFreshName | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFreshName_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFrozenMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithFunction | Agda.TypeChecking.Rules.Def
WithFunctionProblem | Agda.TypeChecking.Rules.Def
withFunctionType | Agda.TypeChecking.With
WithFunCtx | Agda.Syntax.Fixity
WithHiding |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
withHiding | Agda.Syntax.Concrete.Pretty
withHighlightingLevel | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withInterval | Agda.Syntax.Parser.LexActions
withInterval' | Agda.Syntax.Parser.LexActions
withInterval_ | Agda.Syntax.Parser.LexActions
WithK | Agda.Syntax.Common
WithKEnabled | Agda.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
withLayout | Agda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVars | Agda.Syntax.Scope.Monad
withMetaId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withName | Agda.Syntax.Translation.ReflectedToAbstract
withNamedArgsFrom | Agda.Syntax.Common
withNames | Agda.Syntax.Translation.ReflectedToAbstract
withNBackCallStack | Agda.Utils.CallStack
WithNode |
1 (Type/Class) | Agda.TypeChecking.Pretty
2 (Data Constructor) | Agda.TypeChecking.Pretty
withNonEmpty |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Set1
withObject | Agda.Interaction.JSON
WithOnFreeVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithOnFreeVariable_ | Agda.Interaction.Options.Errors
WithOrigin |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
withoutCache | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithoutForce | Agda.Interaction.Base
WithoutK | Agda.Syntax.Common
withoutKeys | Agda.Utils.Map1
WithoutKFlagPrimEraseEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithoutKFlagPrimEraseEquality_ | Agda.Interaction.Options.Warnings
withoutKOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutPrintingGeneralization | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutPrivates | Agda.Syntax.Scope.Base
WithP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
withPositivityCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
withPragmaOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withRangeOf | Agda.Syntax.Position
withRangesOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
withRangesOfQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
withReduced | Agda.TypeChecking.Constraints
WithRHS | Agda.Syntax.Abstract
WithRHSS | Agda.Syntax.Abstract
withScientific | Agda.Interaction.JSON
withScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShadowingNameTCM | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShowAllArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShowAllArguments' | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withSome | Agda.Utils.IndexedList
withStandardLock | Agda.Syntax.Common
withTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withTerminationCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
withText | Agda.Interaction.JSON
withTopLevelModule | Agda.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
withUniverseCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
withUsableVars | Agda.Termination.Monad
withVar | Agda.Syntax.Translation.ReflectedToAbstract
withVarOcc | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
withVars | Agda.Syntax.Translation.ReflectedToAbstract
Wk | Agda.Syntax.Internal, Agda.TypeChecking.Substitute
wkS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
woOrigin | Agda.Syntax.Common
word64View | Agda.Syntax.Treeless, Agda.Compiler.Backend
wordBounded | Agda.Interaction.Highlighting.Vim
wordsBy | Agda.Utils.List1
workOnTypes | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
workOnTypes' | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
woThing | Agda.Syntax.Common
writeFile | Agda.Utils.IO.UTF8
writeIORef | Agda.Utils.IORef
writeModule | Agda.Compiler.JS.Compiler
writeTextToFile | Agda.Utils.IO.UTF8
writeToCurrentLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
writeToTempFile | Agda.Utils.IO.TempFile
writeUnifyLog | Agda.TypeChecking.Rules.LHS.Unify.Types
WrongAnnotationInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongAnnotationInLambda_ | Agda.Interaction.Options.Errors
WrongArgInfoForPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongArgInfoForPrimitive_ | Agda.Interaction.Options.Errors
WrongCohesionInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongCohesionInLambda_ | Agda.Interaction.Options.Errors
WrongContentBlock | Agda.Syntax.Concrete.Definitions.Errors
WrongContentBlock_ | Agda.Interaction.Options.Errors
WrongDefinition | Agda.Syntax.Concrete.Definitions.Errors
WrongDefinition_ | Agda.Interaction.Options.Errors
WrongHidingInApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInApplication_ | Agda.Interaction.Options.Errors
WrongHidingInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLambda_ | Agda.Interaction.Options.Errors
WrongHidingInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLHS_ | Agda.Interaction.Options.Errors
WrongHidingInProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInProjection_ | Agda.Interaction.Options.Errors
WrongInstanceDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongInstanceDeclaration_ | Agda.Interaction.Options.Warnings
WrongIrrelevanceInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongIrrelevanceInLambda_ | Agda.Interaction.Options.Errors
WrongNamedArgument | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNamedArgument_ | Agda.Interaction.Options.Errors
WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNumberOfConstructorArguments_ | Agda.Interaction.Options.Errors
WrongPolarityInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongPolarityInLambda_ | Agda.Interaction.Options.Errors
WrongPragmaFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongPragmaFor_ | Agda.Interaction.Options.Errors
WrongQuantityInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongQuantityInLambda_ | Agda.Interaction.Options.Errors
WrongSharpArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongSharpArity_ | Agda.Interaction.Options.Errors
WrongTypeOfMain | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongTypeOfMain_ | Agda.Interaction.Options.Errors
WSM | Agda.Syntax.Scope.Monad