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

Index - N

Name 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
3 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
4 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
5 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
6 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
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
NamedWhereModuleInRefinedContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.Aspect, 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, Agda.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
nameOfSharpAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfTranspAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfUnivAgda.TypeChecking.Monad.Builtin, 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
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.Name, Agda.Syntax.Concrete
nameSuffixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSuffixViewAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
natSizeAgda.Utils.Size
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.Syntax.Common.Pretty
2 (Function)Agda.TypeChecking.Pretty
nestedCommentAgda.Syntax.Parser.Comments
NeutralArgAgda.TypeChecking.MetaVars
NeverColourAgda.Interaction.Options
NeverProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
newOptionNameAgda.Interaction.Options
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
nextLocalMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Syntax.Concrete.Definitions
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
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
NiceOpaqueAgda.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
NiceState 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Monad
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Monad
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.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
NoArgAgda.Interaction.Options
noAugAgda.Termination.CallMatrix
NoBindingForBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoBindingForPrimitiveAgda.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
NoCubicalAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
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.Positivity
5 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
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
NoErasedMatchesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoEtaAgda.Syntax.Common
noFixityAgda.Syntax.Common
noFixity'Agda.Syntax.Common
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
NoInfoAgda.TypeChecking.Coverage.SplitClause
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep_termAgda.Auto.Typecheck
NoKAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nolamAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
NoLeftInvAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
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
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
NoOpaqueAgda.Syntax.Common
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
noProfileOptionsAgda.Utils.ProfileOptions
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
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.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
notAgda.Utils.Boolean
not'Agda.Syntax.Parser.Alex
NotADatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotAffectedByOpaqueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotAffectedByOpaque_Agda.Interaction.Options.Warnings
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
NotationPartAgda.Syntax.Common
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
notDominatedAgda.Utils.Favorites
noteAgda.Syntax.Common.Aspect, Agda.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.BoolSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.SmallSet
NotOnlyTokenBasedAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
NotOverappliedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotPBAgda.Auto.NarrowingSearch
NotProjectionLikePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
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
notSoPrettySigCubicalNotErasureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
notUnderOpaqueAgda.TypeChecking.Monad.Signature, 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
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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.JSON
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