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

Index - W

waitokAgda.Auto.NarrowingSearch
wakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
wakeIrrelevantVarsAgda.TypeChecking.Irrelevance
wakeupConstraintsAgda.TypeChecking.Constraints
wakeupConstraints_Agda.TypeChecking.Constraints
wakeupListenerAgda.TypeChecking.MetaVars
Warnings 
1 (Type/Class)Agda.TypeChecking.Errors
2 (Data Constructor)Agda.TypeChecking.Errors
warningsToErrorAgda.TypeChecking.Errors
warshallAgda.Utils.Warshall
warshallGAgda.Utils.Warshall
WeakAgda.Auto.Syntax
weakAgda.Auto.Syntax
weakarglistAgda.Auto.Syntax
weakelrAgda.Auto.Syntax
weakenAgda.Auto.Convert
weakensAgda.Auto.Convert
weakiAgda.Auto.Syntax
weaklyAgda.TypeChecking.MetaVars.Occurs
WeaklyRigidAgda.TypeChecking.Free
weaklyRigidVarsAgda.TypeChecking.Free
Weight 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
wellFormedIndicesAgda.TypeChecking.Rules.LHS.Split
whatInductionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
whenAgda.Utils.Monad
whenConstraintsAgda.TypeChecking.Constraints
whenFailAgda.Utils.QuickCheck
whenFail'Agda.Utils.QuickCheck
whenJust 
1 (Function)Agda.Utils.Maybe.Strict
2 (Function)Agda.Utils.Maybe
whenJustM 
1 (Function)Agda.Utils.Maybe.Strict
2 (Function)Agda.Utils.Maybe
whenMAgda.Utils.Monad
when_Agda.Utils.Monad
WhereClauseAgda.Syntax.Concrete
WhereClause'Agda.Syntax.Concrete
whileLeftAgda.Utils.Either
WhyInScopeAgda.Syntax.Scope.Base
whyInScope 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.InteractionTop
WildMPAgda.TypeChecking.Coverage.Match
WildP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
WildVAgda.Syntax.Concrete.Operators.Parser
WithAgda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
withAnonymousModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
WithApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
withAppBracketsAgda.Syntax.Fixity
WithArgCtxAgda.Syntax.Fixity
withArgsFromAgda.Syntax.Common
WithArity 
1 (Type/Class)Agda.TypeChecking.CompiledClause
2 (Data Constructor)Agda.TypeChecking.CompiledClause
WithClausePatternMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WithColorsAgda.Syntax.Concrete
withConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
withContextPrecedenceAgda.Syntax.Scope.Monad
withCurrentFileAgda.Interaction.InteractionTop
withCurrentModule 
1 (Function)Agda.Syntax.Scope.Monad
2 (Function)Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
withCurrentModule'Agda.Syntax.Scope.Monad
withDisplayFormAgda.TypeChecking.With
withEnvAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
WithExprAgda.Syntax.Concrete
withExtendedOccEnvAgda.TypeChecking.Positivity
withFreshAgda.Utils.Fresh
WithFunctionAgda.TypeChecking.Rules.Def
WithFunctionProblemAgda.TypeChecking.Rules.Def
withFunctionTypeAgda.TypeChecking.With
WithFunCtxAgda.Syntax.Fixity
withHighlightingLevelAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
withImportPathAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
withinAgda.Utils.QuickCheck
withIncreasedModuleNestingLevelAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
withInteractionIdAgda.Interaction.BasicOps
withIntervalAgda.Syntax.Parser.LexActions
withInterval'Agda.Syntax.Parser.LexActions
withInterval_Agda.Syntax.Parser.LexActions
withLayoutAgda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVarsAgda.Syntax.Scope.Monad
withMetaIdAgda.Interaction.BasicOps
withMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
withMetaInfo'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
withNamedArgsFromAgda.Syntax.Common
WithNode 
1 (Type/Class)Agda.TypeChecking.Positivity
2 (Data Constructor)Agda.TypeChecking.Positivity
WithoutKErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WithoutKExceptionAgda.TypeChecking.Rules.LHS.Unify
withRangeOfAgda.Syntax.Position
withRangesOfAgda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
withRangesOfQAgda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
WithRHSAgda.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
withShowAllArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
withSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
withTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
withTypesFromAgda.TypeChecking.Rules.LHS.Split
withUsableVarsAgda.Termination.Monad
WkAgda.TypeChecking.Substitute
wkSAgda.TypeChecking.Substitute
wordBoundaryAgda.Compiler.JS.Parser
wordBoundedAgda.Interaction.Highlighting.Vim
wordsByAgda.Utils.List
workOnTypesAgda.TypeChecking.Irrelevance
workOnTypes'Agda.TypeChecking.Irrelevance
Wrap 
1 (Type/Class)Agda.Compiler.MAlonzo.Pretty
2 (Data Constructor)Agda.Compiler.MAlonzo.Pretty
writeFileAgda.Utils.IO.UTF8
writeInterfaceAgda.Interaction.Imports
writeModule 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
WrongDefinitionAgda.Syntax.Concrete.Definitions
WrongHidingInApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongHidingInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongHidingInLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongIrrelevanceInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongNamedArgumentAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongNumberOfConstructorArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongParametersAgda.Syntax.Concrete.Definitions
WSMAgda.Syntax.Scope.Monad