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 |
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 |
warshall | Agda.Utils.Warshall |
warshallG | Agda.Utils.Warshall |
weakly | Agda.TypeChecking.MetaVars.Occurs |
WeaklyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
Weight | |
1 (Type/Class) | Agda.Utils.Warshall |
2 (Type/Class) | 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 |
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 |
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 |
WithClausePatternMismatch | 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 |
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 |
withObject | Agda.Interaction.JSON |
WithOnFreeVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 | |
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 |
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 |
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 |
WrongArgInfoForPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongCohesionInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongContentBlock | Agda.Syntax.Concrete.Definitions.Errors |
WrongDefinition | Agda.Syntax.Concrete.Definitions.Errors |
WrongHidingInApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongHidingInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongHidingInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongHidingInProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
WrongNamedArgument | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WrongQuantityInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
WSM | Agda.Syntax.Scope.Monad |