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 - N

Name
1 (Type/Class)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class)	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
4 (Data Constructor)	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
5 (Data Constructor)	Agda.Interaction.Highlighting.Precise
nameBindingSite	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
nameConcrete	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
Named
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
named	Agda.Syntax.Common
NamedArg	Agda.Syntax.Common
namedArg	Agda.Syntax.Common
NamedClause	Agda.Syntax.Translation.InternalToAbstract
NamedMeta
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
namedThing	Agda.Syntax.Common
nameFixity	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
nameFreq	Agda.TypeChecking.Test.Generators
NameFreqs
1 (Type/Class)	Agda.TypeChecking.Test.Generators
2 (Data Constructor)	Agda.TypeChecking.Test.Generators
nameFreqs	Agda.TypeChecking.Test.Generators
NameId
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
nameId	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
NameKind	Agda.Interaction.Highlighting.Precise
nameModifiers	Agda.Interaction.InteractionTop
nameOf	Agda.Syntax.Common
nameOfBV	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
nameOfFlat	Agda.TypeChecking.Monad.Builtin
nameOfInf	Agda.TypeChecking.Monad.Builtin
nameOfSharp	Agda.TypeChecking.Monad.Builtin
NamePart	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameParts	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NamesInScope	Agda.Syntax.Scope.Base
namesInScope	Agda.Syntax.Scope.Base
NameSpace
1 (Type/Class)	Agda.Syntax.Scope.Base
2 (Data Constructor)	Agda.Syntax.Scope.Base
nameSpaceAccess	Agda.Syntax.Scope.Base
NameSpaceId	Agda.Syntax.Scope.Base
nameStringParts	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSupply	Agda.Compiler.Epic.CompileState
NameTag	Agda.Syntax.Scope.Base
Nat
1 (Type/Class)	Agda.Auto.Syntax
2 (Type/Class)	Agda.Syntax.Common
3 (Type/Class)	Agda.TypeChecking.Primitive
4 (Data Constructor)	Agda.TypeChecking.Primitive
natPrimTF	Agda.Compiler.Epic.Primitive
natural	Agda.Utils.TestHelpers
NeedOptionCopatterns	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
neg	Agda.TypeChecking.Polarity
negtype	Agda.Auto.Convert
neighbours	Agda.Utils.Graph
nest
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
nestedComment	Agda.Syntax.Parser.Comments
NeutralLevel	Agda.Syntax.Internal
newArgsMeta	Agda.TypeChecking.MetaVars
newArgsMeta'	Agda.TypeChecking.MetaVars
newArgsMetaCtx	Agda.TypeChecking.MetaVars
newArgsMetaCtx'	Agda.TypeChecking.MetaVars
newCTree	Agda.Auto.NarrowingSearch
newEdge	Agda.Utils.Warshall
NewFlex	Agda.Utils.Warshall
newIFSMeta	Agda.TypeChecking.MetaVars
newIFSMetaCtx	Agda.TypeChecking.MetaVars
newLayoutContext	Agda.Syntax.Parser.Layout
newMeta
1 (Function)	Agda.Auto.NarrowingSearch
2 (Function)	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
newMeta'	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
NewModuleName	Agda.Syntax.Translation.ConcreteToAbstract
NewModuleQName
1 (Type/Class)	Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)	Agda.Syntax.Translation.ConcreteToAbstract
NewName	Agda.Syntax.Translation.ConcreteToAbstract
newName	Agda.Compiler.Epic.CompileState
newNamedValueMeta	Agda.TypeChecking.MetaVars
NewNotation	Agda.Syntax.Fixity
newOKHandle	Agda.Auto.NarrowingSearch
newPlaceholder	Agda.Auto.NarrowingSearch
newProblem	Agda.TypeChecking.Constraints
newProblem_	Agda.TypeChecking.Constraints
newPtr	Agda.Utils.Pointer, Agda.Syntax.Internal
newQuestionMark	Agda.TypeChecking.MetaVars
newRecordMeta	Agda.TypeChecking.MetaVars
newRecordMetaCtx	Agda.TypeChecking.MetaVars
newSortMeta	Agda.TypeChecking.MetaVars
newSortMetaCtx	Agda.TypeChecking.MetaVars
newSubConstraints	Agda.Auto.NarrowingSearch
newTelMeta	Agda.TypeChecking.MetaVars
newTypeMeta	Agda.TypeChecking.MetaVars
newTypeMeta_	Agda.TypeChecking.MetaVars
newValueMeta	Agda.TypeChecking.MetaVars
newValueMeta'	Agda.TypeChecking.MetaVars
newValueMetaCtx	Agda.TypeChecking.MetaVars
newValueMetaCtx'	Agda.TypeChecking.MetaVars
nextChar	Agda.Syntax.Parser.LookAhead
nextFresh	Agda.Utils.Fresh
nextName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
nextNode	Agda.Utils.Warshall
nextPolarity	Agda.TypeChecking.Polarity
nextSplit	Agda.TypeChecking.CompiledClause.Compile
nextSuffix	Agda.Utils.Suffix
Nice	Agda.Syntax.Concrete.Definitions
NiceConstructor	Agda.Syntax.Concrete.Definitions
NiceDataSig	Agda.Syntax.Concrete.Definitions
NiceDeclaration	Agda.Syntax.Concrete.Definitions
niceDeclarations	Agda.Syntax.Concrete.Definitions
NiceField	Agda.Syntax.Concrete.Definitions
NiceFunClause	Agda.Syntax.Concrete.Definitions
NiceImport	Agda.Syntax.Concrete.Definitions
NiceModule	Agda.Syntax.Concrete.Definitions
NiceModuleMacro	Agda.Syntax.Concrete.Definitions
NiceMutual	Agda.Syntax.Concrete.Definitions
NiceOpen	Agda.Syntax.Concrete.Definitions
NicePatternSyn	Agda.Syntax.Concrete.Definitions
NicePragma	Agda.Syntax.Concrete.Definitions
NiceRecSig	Agda.Syntax.Concrete.Definitions
NiceTypeSignature	Agda.Syntax.Concrete.Definitions
nmid	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
nmSuggestion	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
No
1 (Data Constructor)	Agda.TypeChecking.Coverage.Match
2 (Data Constructor)	Agda.TypeChecking.Patterns.Match
NoAbs	Agda.Syntax.Internal
NoApp	Agda.TypeChecking.EtaContract
NoBindingForBuiltin	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noblks	Agda.Auto.Typecheck
NoBody	Agda.Syntax.Internal
noCompiledRep	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noConstraints	Agda.TypeChecking.Constraints
Node
1 (Type/Class)	Agda.Utils.Warshall
2 (Type/Class)	Agda.TypeChecking.Positivity
NodeId	Agda.Utils.Warshall
nodeIn	Agda.Utils.Graph
nodeMap	Agda.Utils.Warshall
nodes	Agda.Utils.Graph
NoElim	Agda.TypeChecking.Eliminators
NoExpectedFailure	Agda.Utils.QuickCheck
noFixity	Agda.Syntax.Fixity
NoHighlighting	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoId	Agda.Auto.Syntax
NoInsertNeeded	Agda.TypeChecking.Implicit
NoInv	Agda.TypeChecking.Injectivity
noiotastep	Agda.Auto.Typecheck
noiotastep_term	Agda.Auto.Typecheck
NoLayout	Agda.Syntax.Parser.Monad
noLiterals	Agda.TypeChecking.Test.Generators
noMatchLit	Agda.TypeChecking.Coverage.Match
noModuleName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
noMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
NoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName_	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NonAssoc	Agda.Syntax.Fixity
None	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonEmpty	Agda.Utils.QuickCheck
NonEmptyList	Agda.Utils.QuickCheck
nonfixP	Agda.Syntax.Concrete.Operators.Parser
NonInteractive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonNegative
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
noNotation	Agda.Syntax.Notation
NonPositively	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonStrict	Agda.Syntax.Common
nonStrictToIrr	Agda.TypeChecking.Irrelevance
Nonvariant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
nonvariantToUnusedArg	Agda.TypeChecking.Polarity
nonvariantToUnusedArgInClause	Agda.TypeChecking.Polarity
nonvariantToUnusedArgInDef	Agda.TypeChecking.Polarity
NonZero
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
NoOccurrence	Agda.TypeChecking.Free
NoParseForApplication	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoParseForLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noPatternMatchingOnCodata	Agda.TypeChecking.Rules.LHS
Nope	Agda.Syntax.Info
noPostponing	Agda.TypeChecking.Rules.LHS.Unify
NoPrio	Agda.Auto.NarrowingSearch
noProblemRest	Agda.TypeChecking.Rules.LHS.ProblemRest
noProp	Agda.TypeChecking.Test.Generators
noRange	Agda.Syntax.Position
NoReduction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoRHSRequiresAbsurdPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
norm	Agda.Auto.Convert
normal	Agda.Syntax.Parser.Lexer
NormalHole	Agda.Syntax.Notation
Normalise	Agda.TypeChecking.Reduce
normalise	Agda.TypeChecking.Reduce
Normalised	Agda.Interaction.BasicOps
normaliseStatic	Agda.Compiler.Epic.Static
normalMetaPriority	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noShadowingOfConstructors	Agda.TypeChecking.Rules.LHS
noShrink	Agda.TypeChecking.Test.Generators
NoSuchBuiltinName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchName	Agda.TypeChecking.Implicit
NoSuchPrimitiveFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuffix	Agda.Utils.Suffix
not'	Agda.Syntax.Parser.Alex
NotADatatype	Agda.TypeChecking.Coverage
notAHaskellKind	Agda.Compiler.HaskellTypes
notAHaskellType	Agda.Compiler.HaskellTypes
noTakenNames	Agda.Syntax.Translation.AbstractToConcrete
NotAllowedInMutual	Agda.Syntax.Concrete.Definitions
NotAModuleExpr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAnExpression	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAProperTerm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Notation	Agda.Syntax.Notation
NotAValidLetBinding	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotB	Agda.Auto.NarrowingSearch
NotBlocked	Agda.Syntax.Internal
notBlocked	Agda.Syntax.Internal
NotComparable	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
NotDelayed	Agda.Syntax.Common
note	Agda.Interaction.Highlighting.Precise
notequal	Agda.Auto.CaseSplit
NoTerminationCheckPragma	Agda.Syntax.Concrete
NotForced	Agda.Compiler.Epic.Interface
notForced	Agda.Compiler.Epic.Interface
NotFound	Agda.Interaction.FindFile
NotHidden
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Common
notHiddenFreq	Agda.TypeChecking.Test.Generators
Nothing	Agda.Utils.Maybe
NothingAppliedToHiddenArg	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingAppliedToInstanceArg	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingToPrune	Agda.TypeChecking.MetaVars.Occurs
NothingToSplit	Agda.TypeChecking.Rules.LHS.Problem
nothingToSplitError	Agda.TypeChecking.Rules.LHS.Instantiate
NotImplemented	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInductive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInjective	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notInScope	Agda.Syntax.Scope.Monad
NotLeqSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotM	Agda.Auto.NarrowingSearch
NotPB	Agda.Auto.NarrowingSearch
NotReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notSoNiceDeclaration	Agda.Syntax.Concrete.Definitions
NotStrictlyPositive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotSupported	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoType
1 (Type/Class)	Agda.TypeChecking.Test.Generators
2 (Data Constructor)	Agda.TypeChecking.Test.Generators
NoUnfold	Agda.TypeChecking.MetaVars.Occurs
NoUnify	Agda.TypeChecking.Rules.LHS.Unify
NoWhere	Agda.Syntax.Concrete
NoWithFunction	Agda.TypeChecking.Rules.Def
nowSolvingConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
nPi	Agda.TypeChecking.Primitive
nrBinds	Agda.Compiler.Epic.Injection
nrRel	Agda.Compiler.Epic.NatDetection
nsModules	Agda.Syntax.Scope.Base
nsNames	Agda.Syntax.Scope.Base
null	Agda.Utils.HashMap
Number	Agda.Interaction.Highlighting.Precise
numPars	Agda.Compiler.JS.Compiler
numShrinks	Agda.Utils.QuickCheck
numTests	Agda.Utils.QuickCheck
numVars	Agda.Compiler.JS.Case
numVars'	Agda.Compiler.JS.Case