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

Index - N

Name 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
4 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
5 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
6 (Data Constructor)Agda.Interaction.Highlighting.Precise
nameBindingSiteAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
nameCAgda.TypeChecking.Serialise.Base
nameConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
Named 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
nameDAgda.TypeChecking.Serialise.Base
namedAgda.Syntax.Common
NamedArgAgda.Syntax.Common
namedArgAgda.Syntax.Common
namedArgFromDomAgda.Syntax.Internal
namedArgNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
NamedArgsAgda.Syntax.Internal
NamedBinding 
1 (Type/Class)Agda.Syntax.Concrete.Pretty
2 (Data Constructor)Agda.Syntax.Concrete.Pretty
namedBindingAgda.Syntax.Concrete.Pretty
namedBindsToTelAgda.TypeChecking.Substitute
NamedClause 
1 (Type/Class)Agda.Syntax.Translation.InternalToAbstract
2 (Data Constructor)Agda.Syntax.Translation.InternalToAbstract
namedClausePatsAgda.Syntax.Internal
namedDBVarPAgda.Syntax.Internal
NamedMeta 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
namedMetaOfAgda.Interaction.BasicOps, Agda.Interaction.EmacsTop
NamedNameAgda.Syntax.Common
NamedRigid 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Solve
namedSameAgda.Syntax.Common
namedTelVarsAgda.TypeChecking.Substitute
namedThingAgda.Syntax.Common
namedVarPAgda.Syntax.Internal
Named_Agda.Syntax.Common
nameFieldAAgda.Syntax.Concrete
nameFixityAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
NameId 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
nameId 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
NameInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameIsRecordNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
NameKindAgda.Interaction.Highlighting.Precise
NameMapAgda.Syntax.Scope.Base
NameMetadataAgda.Syntax.Scope.Base
nameNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NameNotModuleAgda.Syntax.Scope.Base
nameOfAgda.Syntax.Common
nameOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfBV'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfFlatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfHCompAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfInfAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfSharpAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfTranspAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NameOrModuleAgda.Syntax.Scope.Base
NamePart 
1 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.TypeChecking.Unquote
namePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameRangeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Names 
1 (Type/Class)Agda.TypeChecking.Names
2 (Type/Class)Agda.Syntax.Translation.ReflectedToAbstract
NamesInAgda.Syntax.Internal.Names
namesInAgda.Syntax.Internal.Names
NamesInScopeAgda.Syntax.Scope.Base
namesInScopeAgda.Syntax.Scope.Base
NameSpace 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
nameSpaceAccessAgda.Syntax.Scope.Base
NameSpaceIdAgda.Syntax.Scope.Base
NamesT 
1 (Type/Class)Agda.TypeChecking.Names
2 (Data Constructor)Agda.TypeChecking.Names
namesToNotationAgda.Syntax.Notation
nameStringPartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NameSupplyAgda.Compiler.MAlonzo.Compiler
NameTagAgda.Syntax.Scope.Base
nameToArgNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
NameToExprAgda.Syntax.Abstract
nameToExprAgda.Syntax.Abstract
nameToPatVarNameAgda.Syntax.Internal
nameToRawNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NAPAgda.Syntax.Abstract.Pattern
NAPs 
1 (Type/Class)Agda.Syntax.Internal
2 (Type/Class)Agda.Syntax.Abstract
Nat 
1 (Type/Class)Agda.Syntax.Common
2 (Type/Class)Agda.Auto.Syntax
3 (Type/Class)Agda.TypeChecking.Primitive
4 (Data Constructor)Agda.TypeChecking.Primitive
natAgda.Compiler.Treeless.EliminateLiteralPatterns
NeedOptionCopatternsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionPropAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionRewritingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
negAgda.TypeChecking.Polarity
NegAppAgda.Utils.Haskell.Syntax
NegativeAgda.TypeChecking.SizedTypes.WarshallSolver
negativeAgda.TypeChecking.SizedTypes.WarshallSolver
NegativeUnificationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
negPlusKViewAgda.Syntax.Treeless, Agda.Compiler.Backend
negtypeAgda.Auto.Convert
neighboursAgda.Utils.Graph.AdjacencyMap.Unidirectional
neighboursMapAgda.Utils.Graph.AdjacencyMap.Unidirectional
nest 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
nestedCommentAgda.Syntax.Parser.Comments
NeutralArgAgda.TypeChecking.MetaVars
NeutralLevelAgda.Syntax.Internal
newAbsAgda.Auto.SearchControl
newAppAgda.Auto.SearchControl
newApp'Agda.Auto.SearchControl
newArgsAgda.Auto.SearchControl
newArgs'Agda.Auto.SearchControl
newArgsMetaAgda.TypeChecking.MetaVars
newArgsMeta'Agda.TypeChecking.MetaVars
newArgsMetaCtxAgda.TypeChecking.MetaVars
newArgsMetaCtx'Agda.TypeChecking.MetaVars
newCTreeAgda.Auto.NarrowingSearch
NewFlexAgda.Utils.Warshall
newInstanceMetaAgda.TypeChecking.MetaVars
newInstanceMetaCtxAgda.TypeChecking.MetaVars
newInteractionMetaArgAgda.TypeChecking.Implicit
newIORefAgda.Utils.IORef
newLamAgda.Auto.SearchControl
newLayoutContextAgda.Syntax.Parser.Layout
newLevelMetaAgda.TypeChecking.MetaVars
newMeta 
1 (Function)Agda.Auto.NarrowingSearch
2 (Function)Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
newMeta'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
newMetaArgAgda.TypeChecking.Implicit
newMetaTCM'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NewModuleNameAgda.Syntax.Translation.ConcreteToAbstract
NewModuleQName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
NewNameAgda.Syntax.Translation.ConcreteToAbstract
newNamedValueMetaAgda.TypeChecking.MetaVars
newNamedValueMeta'Agda.TypeChecking.MetaVars
NewNotation 
1 (Type/Class)Agda.Syntax.Notation
2 (Data Constructor)Agda.Syntax.Notation
newOKHandleAgda.Auto.NarrowingSearch
newPiAgda.Auto.SearchControl
newPlaceholderAgda.Auto.NarrowingSearch
newProblemAgda.TypeChecking.Constraints
newProblem_Agda.TypeChecking.Constraints
newPtrAgda.Utils.Pointer
newQuestionMarkAgda.TypeChecking.MetaVars
newQuestionMark'Agda.TypeChecking.MetaVars
newRecordMetaAgda.TypeChecking.MetaVars
newRecordMetaCtxAgda.TypeChecking.MetaVars
newSectionAgda.TypeChecking.Rules.Def
newSortMetaAgda.TypeChecking.MetaVars
newSortMetaBelowInfAgda.TypeChecking.MetaVars
newSortMetaCtxAgda.TypeChecking.MetaVars
newSubConstraintsAgda.Auto.NarrowingSearch
newTelMetaAgda.TypeChecking.MetaVars
NewTypeAgda.Utils.Haskell.Syntax
newTypeMetaAgda.TypeChecking.MetaVars
newTypeMeta'Agda.TypeChecking.MetaVars
newTypeMeta_Agda.TypeChecking.MetaVars
newValueMetaAgda.TypeChecking.MetaVars
newValueMeta'Agda.TypeChecking.MetaVars
newValueMetaCtxAgda.TypeChecking.MetaVars
newValueMetaCtx'Agda.TypeChecking.MetaVars
nextCharAgda.Syntax.Parser.LookAhead
nextFreshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nextFresh'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nextHoleAgda.Utils.Zipper
nextIsForcedAgda.TypeChecking.Forcing
nextName 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
nextNodeAgda.Utils.Warshall
nextPolarityAgda.TypeChecking.Polarity
nextSplitAgda.TypeChecking.CompiledClause.Compile
nextStrAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nextSuffixAgda.Utils.Suffix
NiceAgda.Syntax.Concrete.Definitions
NiceConstructorAgda.Syntax.Concrete.Definitions
NiceDataDefAgda.Syntax.Concrete.Definitions
NiceDataSigAgda.Syntax.Concrete.Definitions
NiceDeclarationAgda.Syntax.Concrete.Definitions
niceDeclarationsAgda.Syntax.Concrete.Definitions
NiceFieldAgda.Syntax.Concrete.Definitions
NiceFunClauseAgda.Syntax.Concrete.Definitions
NiceGeneralizeAgda.Syntax.Concrete.Definitions
niceHasAbstractAgda.Syntax.Concrete.Definitions
NiceImportAgda.Syntax.Concrete.Definitions
NiceModuleAgda.Syntax.Concrete.Definitions
NiceModuleMacroAgda.Syntax.Concrete.Definitions
NiceMutualAgda.Syntax.Concrete.Definitions
NiceOpenAgda.Syntax.Concrete.Definitions
NicePatternSynAgda.Syntax.Concrete.Definitions
NicePragmaAgda.Syntax.Concrete.Definitions
NiceRecDefAgda.Syntax.Concrete.Definitions
NiceRecSigAgda.Syntax.Concrete.Definitions
NiceTypeSignatureAgda.Syntax.Concrete.Definitions
NiceUnquoteDeclAgda.Syntax.Concrete.Definitions
NiceUnquoteDefAgda.Syntax.Concrete.Definitions
NicifierIssueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NilAgda.Utils.IndexedList
nilListTAgda.Utils.ListT
NKAgda.Syntax.Concrete.Operators.Parser
NLMAgda.TypeChecking.Rewriting.NonLinMatch
nlmEqsAgda.TypeChecking.Rewriting.NonLinMatch
NLMState 
1 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)Agda.TypeChecking.Rewriting.NonLinMatch
nlmSubAgda.TypeChecking.Rewriting.NonLinMatch
NLPatAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NLPatToTermAgda.TypeChecking.Rewriting.NonLinPattern
nlPatToTermAgda.TypeChecking.Rewriting.NonLinPattern
NLPatVarsAgda.TypeChecking.Rewriting.NonLinPattern
nlPatVarsAgda.TypeChecking.Rewriting.NonLinPattern
nlPatVarsUnderAgda.TypeChecking.Rewriting.NonLinPattern
NLPSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NLPType 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nlpTypeSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nlpTypeUnElAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nmidAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nmSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
No 
1 (Data Constructor)Agda.TypeChecking.Patterns.Match
2 (Data Constructor)Agda.TypeChecking.Coverage.Match
NoAbsAgda.Syntax.Internal
noabsAppAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
NoAppAgda.TypeChecking.EtaContract
noApplicationAgda.Compiler.MAlonzo.Compiler
NoArgAgda.Interaction.Options
noAugAgda.Termination.CallMatrix
NoBindingForBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noblksAgda.Auto.Typecheck
noCheckCoverAgda.Compiler.MAlonzo.Primitives
noCompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noConPatternInfoAgda.Syntax.Internal
noConstraintsAgda.TypeChecking.Constraints
NoCoverageCheckAgda.Syntax.Common
NoCoverageCheckPragmaAgda.Syntax.Concrete
noDataDefParamsAgda.Syntax.Abstract
Node 
1 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Type/Class)Agda.Termination.CallGraph
3 (Type/Class)Agda.Utils.Warshall
4 (Type/Class)Agda.TypeChecking.Serialise.Base
5 (Type/Class)Agda.TypeChecking.Positivity
nodeCAgda.TypeChecking.Serialise.Base
nodeDAgda.TypeChecking.Serialise.Base
nodeEAgda.TypeChecking.Serialise.Base
NodeFlexAgda.TypeChecking.SizedTypes.WarshallSolver
nodeFromSizeExprAgda.TypeChecking.SizedTypes.WarshallSolver
NodeIdAgda.Utils.Warshall
NodeInftyAgda.TypeChecking.SizedTypes.WarshallSolver
NodeKAgda.Syntax.Concrete.Operators.Parser.Monad
nodeMapAgda.Utils.Warshall
nodeMemoAgda.TypeChecking.Serialise.Base
NodeRigidAgda.TypeChecking.SizedTypes.WarshallSolver
Nodes 
1 (Type/Class)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Data Constructor)Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
nodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
nodeToSizeExprAgda.TypeChecking.SizedTypes.WarshallSolver
NodeZeroAgda.TypeChecking.SizedTypes.WarshallSolver
NoEllipsisAgda.Syntax.Common
NoEtaAgda.Syntax.Common
noFixityAgda.Syntax.Common
noFixity'Agda.Syntax.Common
noFreeVariablesAgda.Syntax.Common
noFunctionsIntoSizeAgda.TypeChecking.Rules.Term
NoFunSigAgda.Syntax.Abstract
NoGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoGeneralizeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noGeneralizedVarsIfLetOpenAgda.Syntax.Scope.Monad
NoHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noHighlightingInRangeAgda.Interaction.Highlighting.Precise
NoIdAgda.Auto.Syntax
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep_termAgda.Auto.Typecheck
nolamAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
NoLayoutAgda.Syntax.Parser.Monad
NoMetadataAgda.Syntax.Scope.Base
noMetasAgda.Syntax.Internal.MetaVars
noModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
noMsgAgda.Utils.Except
noMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonAgda.Syntax.Concrete.Operators.Parser
NoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName_Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NonAssocAgda.Syntax.Common
NonCanonicalAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoneAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonFatalErrorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nonFatalErrorsAgda.TypeChecking.Warnings
NonfixKAgda.Syntax.Concrete.Operators.Parser.Monad
NonfixNotationAgda.Syntax.Notation
nonIncreasingAgda.Termination.Order
NonInteractiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nonLinMatchAgda.TypeChecking.Rewriting.NonLinMatch
NoNotationAgda.Syntax.Notation
noNotationAgda.Syntax.Common
nonRecursiveRecordAgda.TypeChecking.Records
NonStrictAgda.Syntax.Common
nonStrictToIrrAgda.Syntax.Common
nonStrictToRelAgda.Syntax.Common
NonTerminatingAgda.Syntax.Common
NonTerminatingReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonvariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoOutputTypeNameAgda.TypeChecking.Telescope
NoOverlapAgda.Syntax.Common
NoParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoParseForLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoPlaceholderAgda.Syntax.Common
noPlaceholderAgda.Syntax.Common
NoPositivityCheckAgda.Syntax.Common
NoPositivityCheckPragmaAgda.Syntax.Concrete
NoPrioAgda.Auto.NarrowingSearch
noProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
NoProjectedVarAgda.TypeChecking.MetaVars
noProjectedVarAgda.TypeChecking.MetaVars
NoProjectionAgda.TypeChecking.ProjectionLike
NoRangeAgda.Syntax.Position
noRangeAgda.Syntax.Position
NoReductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoRHSRequiresAbsurdPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
normalAgda.Syntax.Parser.Lexer
normalFormAgda.Interaction.BasicOps
NormalHoleAgda.Syntax.Common
NormaliseAgda.TypeChecking.Reduce
normaliseAgda.TypeChecking.Reduce
normalise'Agda.TypeChecking.Reduce
normaliseBAgda.TypeChecking.Reduce
NormalisedAgda.Interaction.Base
normaliseNaNAgda.Utils.Float
NormaliseProjPAgda.TypeChecking.Records
normaliseProjPAgda.TypeChecking.Records, Agda.TypeChecking.Coverage
normalizeNamesAgda.Compiler.Treeless.NormalizeNames
normalMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noSectionAgda.Syntax.Notation
NoSimplificationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchBuiltinNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchNameAgda.TypeChecking.Implicit
NoSuchPrimitiveFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuffixAgda.Utils.Suffix
not'Agda.Syntax.Parser.Alex
NotADatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notaFixityAgda.Syntax.Notation
notaIsOperatorAgda.Syntax.Notation
noTakenNamesAgda.Syntax.Translation.AbstractToConcrete
NotAllowedInMutualAgda.Syntax.Concrete.Definitions
NotAllowedInMutual_Agda.Interaction.Options.Warnings
NotAModuleExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notaNameAgda.Syntax.Notation
notaNamesAgda.Syntax.Notation
NotAnExpressionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotAProjectionPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotAProperTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotationAgda.Syntax.Common
notationAgda.Syntax.Notation
NotationKindAgda.Syntax.Notation
notationKindAgda.Syntax.Notation
notationNamesAgda.Syntax.Notation
NotationSection 
1 (Type/Class)Agda.Syntax.Notation
2 (Data Constructor)Agda.Syntax.Notation
NotAValidLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotBAgda.Auto.NarrowingSearch
NotBlocked 
1 (Data Constructor)Agda.Syntax.Internal
2 (Type/Class)Agda.Syntax.Internal
notBlockedAgda.Syntax.Internal
NotBlockedOnResultAgda.TypeChecking.Coverage.Match
notBlocked_Agda.Syntax.Internal
NotCheckedTargetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotComparableAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotDelayedAgda.Syntax.Common
notDominatedAgda.Utils.Favorites
noteAgda.Interaction.Highlighting.Precise
notequalAgda.Auto.CaseSplit
notequal'Agda.Auto.CaseSplit
NoTerminationCheckAgda.Syntax.Common
NotForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotFoundAgda.Interaction.FindFile
NotFreeAgda.TypeChecking.Free.Reduce
NotHiddenAgda.Syntax.Common
Nothing 
1 (Data Constructor)Agda.Utils.Maybe
2 (Data Constructor)Agda.Utils.Maybe.Strict
NothingAppliedToHiddenArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NothingAppliedToInstanceArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NothingToPruneAgda.TypeChecking.MetaVars.Occurs
NotImplementedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotInjectiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotInScope 
1 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notInScopeErrorAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotInScopeWAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notInScopeWarningAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotInScope_Agda.Interaction.Options.Warnings
NotInstanceDefAgda.Syntax.Common
NotLeqSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotMAgda.Auto.NarrowingSearch
NotMacroDefAgda.Syntax.Common
NotMainAgda.Compiler.Common, Agda.Compiler.Backend
NotMainInterfaceAgda.Interaction.Imports
notMaskedAgda.Termination.Monad
notMember 
1 (Function)Agda.Utils.Bag
2 (Function)Agda.Utils.SmallSet
NotOnlyTokenBasedAgda.Interaction.Highlighting.Precise
NotOverappliedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotPBAgda.Auto.NarrowingSearch
NotReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notShadowedLocalAgda.Syntax.Scope.Base
notShadowedLocalsAgda.Syntax.Scope.Base
notSoNiceDeclarationsAgda.Syntax.Concrete.Definitions
NotStrictlyPositiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotStrictlyPositive_Agda.Interaction.Options.Warnings
NotSupportedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotValidBeforeFieldAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notVisibleAgda.Syntax.Common
NotWorseAgda.Termination.Order
notWorseAgda.Termination.Order
NoUnfoldAgda.TypeChecking.MetaVars.Occurs
NoUnifyAgda.TypeChecking.Rules.LHS.Unify
NoUniverseCheckAgda.Syntax.Common
NoUniverseCheckPragmaAgda.Syntax.Concrete
noUserQuantityAgda.Syntax.Common
NoWarnAgda.Syntax.Concrete.Fixity
NoWarningsAgda.Interaction.Imports
noWarningsAgda.Interaction.Options.Warnings
nowDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoWhereAgda.Syntax.Concrete
noWhereDeclsAgda.Syntax.Abstract
NoWithFunctionAgda.TypeChecking.Rules.Def
nowSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nPiAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
nPi'Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
nsInScopeAgda.Syntax.Scope.Base
nsModulesAgda.Syntax.Scope.Base
nsNamesAgda.Syntax.Scope.Base
nubOnAgda.Utils.List
NullAgda.Utils.Null
null 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.Null
4 (Function)Agda.Utils.SmallSet
NumberAgda.Interaction.Highlighting.Precise
numberOfWithPatternsAgda.Syntax.Concrete.Pattern
numberPatVarsAgda.Syntax.Internal.Pattern
NumGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NumHolesAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
numHolesAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete