Agda-2.6.2.2: 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
nameCanonicalAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
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
namedBindsToTel1Agda.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
NameKind 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Type/Class)Agda.Compiler.MAlonzo.Misc
NameKindsAgda.Interaction.Highlighting.FromAbstract
NameMapAgda.Syntax.Scope.Base
NameMapEntry 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
NameMetadataAgda.Syntax.Scope.Base
nameNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NameNotModuleAgda.Syntax.Scope.Base
NameOfAgda.Syntax.Common
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
nameOfPropAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfSetAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfSetOmegaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfSharpAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfSSetAgda.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
namePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameRangeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NamesAgda.TypeChecking.Names
NamesInAgda.Syntax.Internal.Names
namesInAgda.Syntax.Internal.Names
namesIn'Agda.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
nameSuffixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSuffixViewAgda.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
NAPs1Agda.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
NeedOptionTwoLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
neverUnblockAgda.Syntax.Internal.Blockers, Agda.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
newLayoutBlockAgda.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
nextNameIdAgda.Syntax.Concrete.Definitions.Monad
nextNodeAgda.Utils.Warshall
nextPolarityAgda.TypeChecking.Polarity
nextRawNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nextSplitAgda.TypeChecking.CompiledClause.Compile
nextSuffixAgda.Utils.Suffix
Nice 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Monad
NiceConstructorAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceDataDefAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceDataSigAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceDeclarationAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
niceDeclarationsAgda.Syntax.Concrete.Definitions
NiceEnv 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Monad
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Monad
NiceFieldAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceFunClauseAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceGeneralizeAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
niceHasAbstractAgda.Syntax.Concrete.Definitions
NiceImportAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceLoneConstructorAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceModuleAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceModuleMacroAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceMutualAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceOpenAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NicePatternSynAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NicePragmaAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceRecDefAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceRecSigAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceTypeSignatureAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceUnquoteDeclAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceUnquoteDefAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
niceWarnAgda.Syntax.Concrete.Definitions.Monad
niceWarningAgda.Syntax.Concrete.Definitions.Monad
NiceWarningsAgda.Syntax.Concrete.Definitions.Monad
NicifierIssueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NilAgda.Utils.IndexedList
nilListTAgda.Utils.ListT
NKAgda.Syntax.Concrete.Operators.Parser
NLM 
1 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)Agda.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
NoFloatAgda.Compiler.MAlonzo.Compiler
noFreeVariablesAgda.Syntax.Common
NoGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoGeneralizeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noGeneralizedVarsIfLetOpenAgda.Syntax.Scope.Monad
NoGuardednessFlagAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoGuardednessFlag_Agda.Interaction.Options.Warnings
NoHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoIdAgda.Auto.Syntax
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep_termAgda.Auto.Typecheck
nolamAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
noLoneSigsAgda.Syntax.Concrete.Definitions.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
noModuleNameHashAgda.Syntax.Common
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
nonConstrainingAgda.TypeChecking.Constraints
NoneAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nonEmptyAgda.Utils.List1
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
NoNoErrorAgda.Interaction.Options.Warnings
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
NoPostfixAgda.TypeChecking.ProjectionLike
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
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.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
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.Errors, Agda.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.Blockers, Agda.Syntax.Internal
2 (Type/Class)Agda.Syntax.Internal
notBlockedAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
NotBlocked'Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
NotBlockedOnResultAgda.TypeChecking.Coverage.Match
notBlocked_Agda.Syntax.Internal.Blockers, 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
NotErasedAgda.Syntax.Common
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
NotInMutualAgda.Syntax.Concrete.Definitions.Types
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
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
NoUnusedAgda.Compiler.MAlonzo.Misc
noUserQuantityAgda.Syntax.Common
NoWarnAgda.Syntax.Concrete.Fixity
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
nubAgda.Utils.List1
nubAndDuplicatesOnAgda.Utils.List
nubByAgda.Utils.List1
nubM 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
nubOnAgda.Utils.List
Null 
1 (Data Constructor)Agda.Interaction.JSON
2 (Type/Class)Agda.Utils.Null
3 (Data Constructor)Agda.Compiler.JS.Syntax
null 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.Null
4 (Function)Agda.Utils.SmallSet
Number 
1 (Data Constructor)Agda.Interaction.JSON
2 (Data Constructor)Agda.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