Agda-2.6.2.2.20221106: 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, Agda.Syntax.Concrete.Name
3 (Data Constructor)Agda.Syntax.Concrete, Agda.Syntax.Concrete.Name
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.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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, Agda.Syntax.Concrete.Name
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
NameInScopeAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
nameInScopeAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
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, Agda.Syntax.Concrete.Name
NameNotModuleAgda.Syntax.Scope.Base
NameOfAgda.Syntax.Common
nameOfAgda.Syntax.Common
nameOfBVAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
nameOfBV'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
nameOfFlatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfHCompAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nameOfInfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfPropAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfSetAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfSetOmegaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfSharpAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfSSetAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
nameOfTranspAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NameOrModuleAgda.Syntax.Scope.Base
NamePart 
1 (Type/Class)Agda.Syntax.Concrete, Agda.Syntax.Concrete.Name
2 (Data Constructor)Agda.TypeChecking.Unquote
NamePartsAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
namePartsAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
nameRangeAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
nameRootAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
NamesAgda.TypeChecking.Names
namesAndMetasInAgda.Syntax.Internal.Names
namesAndMetasIn'Agda.Syntax.Internal.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, Agda.Syntax.Concrete.Name
nameSuffixAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
nameSuffixViewAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
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, Agda.Syntax.Concrete.Name
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.Compiler.Backend, Agda.TypeChecking.Monad
NeedOptionPropAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NeedOptionRewritingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NeedOptionTwoLevelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NegAppAgda.Utils.Haskell.Syntax
NegativeAgda.TypeChecking.SizedTypes.WarshallSolver
negativeAgda.TypeChecking.SizedTypes.WarshallSolver
NegativeUnificationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
NeverProjectionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
newMeta'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
newMetaArgAgda.TypeChecking.Implicit
newMetaTCM'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad
nextFresh'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nextHoleAgda.Utils.Zipper
nextIsForcedAgda.TypeChecking.Forcing
nextLocalMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
nextName 
1 (Function)Agda.Syntax.Concrete, Agda.Syntax.Concrete.Name
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, Agda.Syntax.Concrete.Name
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
NiceUnquoteDataAgda.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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
NLPType 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nlpTypeSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nlpTypeUnElAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nmidAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nmSuggestionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
noblksAgda.Auto.Typecheck
noCheckCoverAgda.Compiler.MAlonzo.Primitives
noCompiledRepAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
noConPatternInfoAgda.Syntax.Internal
noConstraintsAgda.TypeChecking.Constraints
NoCoverageCheckAgda.Syntax.Common
NoCoverageCheckPragmaAgda.Syntax.Concrete
NoCubicalAgda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
noDataDefParamsAgda.Syntax.Abstract
Node 
1 (Type/Class)Agda.Termination.CallGraph
2 (Type/Class)Agda.Utils.Warshall
3 (Type/Class)Agda.TypeChecking.Serialise.Base
4 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
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.Compiler.Backend, Agda.TypeChecking.Monad
NoGeneralizeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
noGeneralizedVarsIfLetOpenAgda.Syntax.Scope.Monad
NoGuardednessFlagAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoGuardednessFlag_Agda.Interaction.Options.Warnings
NoHighlightingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoIdAgda.Auto.Syntax
NoInfoAgda.TypeChecking.Coverage.SplitClause
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep_termAgda.Auto.Typecheck
nolamAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
NoLeftInvAgda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
NonAgda.Syntax.Concrete.Operators.Parser
NoNameAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
noNameAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
noName_Agda.Syntax.Concrete, Agda.Syntax.Concrete.Name
NonAssocAgda.Syntax.Common
NonCanonicalAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nonConstrainingAgda.TypeChecking.Constraints
NoneAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NonEmptyAgda.Utils.List1
nonEmptyAgda.Utils.List1
NonFatalErrorsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
nonFatalErrorsAgda.TypeChecking.Warnings
NonfixKAgda.Syntax.Concrete.Operators.Parser.Monad
NonfixNotationAgda.Syntax.Notation
nonIncreasingAgda.Termination.Order
NonInteractiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
NonvariantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoOutputTypeNameAgda.TypeChecking.Telescope
NoOverlapAgda.Syntax.Common
NoParseForApplicationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoParseForLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoPlaceholderAgda.Syntax.Common
noPlaceholderAgda.Syntax.Common
NoPositivityCheckAgda.Syntax.Common
NoPositivityCheckPragmaAgda.Syntax.Concrete
NoPostfixAgda.TypeChecking.ProjectionLike
NoPrioAgda.Auto.NarrowingSearch
noProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
noProfileOptionsAgda.Utils.ProfileOptions
NoProjectedVarAgda.TypeChecking.MetaVars
noProjectedVarAgda.TypeChecking.MetaVars
NoProjectionAgda.TypeChecking.ProjectionLike
NoRangeAgda.Syntax.Position
noRangeAgda.Syntax.Position
NoReductionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoRHSRequiresAbsurdPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
normalAgda.Syntax.Parser.Lexer
normalFormAgda.Interaction.BasicOps
NormaliseAgda.TypeChecking.Reduce
normaliseAgda.TypeChecking.Reduce
normalise'Agda.TypeChecking.Reduce
NormalisedAgda.Interaction.Base
NormaliseProjPAgda.TypeChecking.Records
normaliseProjPAgda.TypeChecking.Records, Agda.TypeChecking.Coverage
normalizeNamesAgda.Compiler.Treeless.NormalizeNames
normalMetaPriorityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
noSectionAgda.Syntax.Notation
NoSimplificationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoSuchBuiltinNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoSuchModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NoSuchNameAgda.TypeChecking.Implicit
NoSuchPrimitiveFunctionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
notaNameAgda.Syntax.Notation
notaNamesAgda.Syntax.Notation
NotAnExpressionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotAProjectionPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotAProperTermAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotationAgda.Syntax.Common
notationAgda.Syntax.Notation
NotationKindAgda.Syntax.Notation
notationKindAgda.Syntax.Notation
notationNamesAgda.Syntax.Notation
NotationPartAgda.Syntax.Common
NotationSection 
1 (Type/Class)Agda.Syntax.Notation
2 (Data Constructor)Agda.Syntax.Notation
NotAValidLetBindingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
NotComparableAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
NothingAppliedToInstanceArgAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NothingToPruneAgda.TypeChecking.MetaVars.Occurs
NotImplementedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotInjectiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotInMutualAgda.Syntax.Concrete.Definitions.Types
NotInScope 
1 (Data Constructor)Agda.Syntax.Concrete, Agda.Syntax.Concrete.Name
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
notInScopeErrorAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotInScopeWAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
notInScopeWarningAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotInScope_Agda.Interaction.Options.Warnings
NotInstanceDefAgda.Syntax.Common
NotLeqSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotMAgda.Auto.NarrowingSearch
NotMacroDefAgda.Syntax.Common
NotMainAgda.Compiler.Backend, Agda.Compiler.Common
notMaskedAgda.Termination.Monad
notMember 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.SmallSet
NotOnlyTokenBasedAgda.Interaction.Highlighting.Precise
NotOverappliedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotPBAgda.Auto.NarrowingSearch
NotProjectionLikePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
NotReducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
notReducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
notShadowedLocalAgda.Syntax.Scope.Base
notShadowedLocalsAgda.Syntax.Scope.Base
notSoNiceDeclarationsAgda.Syntax.Concrete.Definitions
NotStrictlyPositiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotStrictlyPositive_Agda.Interaction.Options.Warnings
NotSupportedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NotValidBeforeFieldAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
NoWhereAgda.Syntax.Concrete
noWhereDeclsAgda.Syntax.Abstract
NoWithFunctionAgda.TypeChecking.Rules.Def
nowSolvingConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
nPiAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
nPi'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
nsInScopeAgda.Syntax.Scope.Base
nsModulesAgda.Syntax.Scope.Base
nsNamesAgda.Syntax.Scope.Base
nubAgda.Utils.List1
nubAndDuplicatesOnAgda.Utils.List
nubByAgda.Utils.List1
nubFavouriteOnAgda.Utils.List
nubM 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
nubOnAgda.Utils.List
Null 
1 (Type/Class)Agda.Utils.Null
2 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Data Constructor)Agda.Interaction.JSON
null 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BoolSet
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.Null
5 (Function)Agda.Utils.SmallSet
Number 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.JSON
numberOfWithPatternsAgda.Syntax.Concrete.Pattern
numberPatVarsAgda.Syntax.Internal.Pattern
NumGeneralizableArgsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
NumHolesAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
numHolesAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name