waitok | Agda.Auto.NarrowingSearch |
wakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
wakeIrrelevantVars | Agda.TypeChecking.Irrelevance |
wakeupConstraints | Agda.TypeChecking.Constraints |
wakeupConstraints_ | Agda.TypeChecking.Constraints |
wakeupListener | Agda.TypeChecking.MetaVars |
walkSatisfying | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
Warnings | |
1 (Type/Class) | Agda.TypeChecking.Errors |
2 (Data Constructor) | Agda.TypeChecking.Errors |
warningsToError | Agda.TypeChecking.Errors |
warshall | Agda.Utils.Warshall |
warshallG | Agda.Utils.Warshall |
Weak | Agda.Auto.Syntax |
weak | Agda.Auto.Syntax |
weakarglist | Agda.Auto.Syntax |
weakelr | Agda.Auto.Syntax |
weaken | Agda.Auto.Convert |
weakens | Agda.Auto.Convert |
weaki | Agda.Auto.Syntax |
weakly | Agda.TypeChecking.MetaVars.Occurs |
WeaklyRigid | |
1 (Data Constructor) | Agda.TypeChecking.Free.Lazy |
2 (Data Constructor) | Agda.TypeChecking.Free.Old |
3 (Data Constructor) | Agda.TypeChecking.Free |
weaklyRigidVars | |
1 (Function) | Agda.TypeChecking.Free.Old |
2 (Function) | Agda.TypeChecking.Free |
Weight | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
2 (Type/Class) | Agda.Utils.Warshall |
wfAfterTel | Agda.TypeChecking.Rules.Def |
wfBeforeTel | Agda.TypeChecking.Rules.Def |
wfClauses | Agda.TypeChecking.Rules.Def |
wfExprs | Agda.TypeChecking.Rules.Def |
wfExprTypes | Agda.TypeChecking.Rules.Def |
wfName | Agda.TypeChecking.Rules.Def |
wfParentName | Agda.TypeChecking.Rules.Def |
wfParentPats | 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 |
whatInduction | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
when | Agda.Utils.Monad |
whenConstraints | Agda.TypeChecking.Constraints |
whenFail | Agda.Utils.QuickCheck |
whenFail' | Agda.Utils.QuickCheck |
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 |
when_ | Agda.Utils.Monad |
Where | Agda.TypeChecking.Positivity |
WhereClause | Agda.Syntax.Concrete |
WhereClause' | Agda.Syntax.Concrete |
whileLeft | Agda.Utils.Either |
WhyInScope | Agda.Syntax.Scope.Base |
whyInScope | |
1 (Function) | Agda.Interaction.BasicOps |
2 (Function) | Agda.Interaction.InteractionTop |
WildHole | Agda.Syntax.Notation |
WildMP | Agda.TypeChecking.Coverage.Match |
wildOrUnqualifiedName | Agda.Syntax.Concrete.Operators.Parser |
WildP | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
WildV | Agda.Syntax.Concrete.Operators.Parser |
With | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
withAnonymousModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
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 |
WithClausePatternMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
withConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
withContextPrecedence | Agda.Syntax.Scope.Monad |
withCurrentFile | |
1 (Function) | Agda.Interaction.CommandLine |
2 (Function) | Agda.Interaction.InteractionTop |
withCurrentModule | |
1 (Function) | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
2 (Function) | Agda.Syntax.Scope.Monad |
withCurrentModule' | Agda.Syntax.Scope.Monad |
withDisplayForm | Agda.TypeChecking.With |
withEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
WithExpr | Agda.Syntax.Concrete |
withExtendedOccEnv | Agda.TypeChecking.Positivity |
withFreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
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 |
withHighlightingLevel | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
withImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
within | Agda.Utils.QuickCheck |
withIncreasedModuleNestingLevel | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
withInteractionId | Agda.Interaction.BasicOps |
withInterval | Agda.Syntax.Parser.LexActions |
withInterval' | Agda.Syntax.Parser.LexActions |
withInterval_ | Agda.Syntax.Parser.LexActions |
withLayout | Agda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout |
withLocalVars | Agda.Syntax.Scope.Monad |
withMetaId | Agda.Interaction.BasicOps |
withMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
withMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
withName | Agda.Syntax.Translation.ReflectedToAbstract |
withNamedArgsFrom | Agda.Syntax.Common |
WithNames | Agda.Syntax.Translation.ReflectedToAbstract |
WithNode | |
1 (Type/Class) | Agda.TypeChecking.Pretty |
2 (Data Constructor) | Agda.TypeChecking.Pretty |
WithOnFreeVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WithoutKError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
withRangeOf | Agda.Syntax.Position |
withRangesOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
withRangesOfQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
WithRHS | Agda.Syntax.Abstract |
withScope | |
1 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
2 (Function) | Agda.Syntax.Translation.AbstractToConcrete |
withScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
withShowAllArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
withSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
withTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
withUsableVars | Agda.Termination.Monad |
Wk | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
wkS | Agda.TypeChecking.Substitute |
wordBoundary | Agda.Compiler.JS.Parser |
wordBounded | Agda.Interaction.Highlighting.Vim |
wordsBy | Agda.Utils.List |
workOnTypes | Agda.TypeChecking.Irrelevance |
workOnTypes' | Agda.TypeChecking.Irrelevance |
Wrap | |
1 (Type/Class) | Agda.Compiler.MAlonzo.Pretty |
2 (Data Constructor) | Agda.Compiler.MAlonzo.Pretty |
writeFile | Agda.Utils.IO.UTF8 |
writeInterface | Agda.Interaction.Imports |
writeIORef | Agda.Utils.IORef |
writeModule | |
1 (Function) | Agda.Compiler.JS.Compiler |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
writeToCurrentLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad |
WrongContentBlock | Agda.Syntax.Concrete.Definitions |
WrongDefinition | Agda.Syntax.Concrete.Definitions |
WrongHidingInApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongHidingInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongHidingInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongInstanceDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongIrrelevanceInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongNamedArgument | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
WrongParameters | Agda.Syntax.Concrete.Definitions |
WSM | Agda.Syntax.Scope.Monad |