| 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 |
| 5 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| 6 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| nameC | Agda.TypeChecking.Serialise.Base |
| nameConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| Named | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| nameD | Agda.TypeChecking.Serialise.Base |
| named | Agda.Syntax.Common |
| NamedArg | Agda.Syntax.Common |
| namedArg | Agda.Syntax.Common |
| NamedArgs | Agda.Syntax.Internal |
| NamedClause | |
| 1 (Type/Class) | Agda.Syntax.Translation.InternalToAbstract |
| 2 (Data Constructor) | Agda.Syntax.Translation.InternalToAbstract |
| namedClausePats | Agda.Syntax.Internal |
| namedDBVarP | Agda.Syntax.Internal |
| NamedDot | Agda.Syntax.Abstract |
| NamedDotPattern | Agda.Syntax.Abstract |
| NamedMeta | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NamedRigid | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Solve |
| namedTelVars | Agda.TypeChecking.Substitute |
| namedThing | Agda.Syntax.Common |
| namedVarP | Agda.Syntax.Internal |
| Named_ | Agda.Syntax.Common |
| nameExpr | Agda.Syntax.Abstract |
| nameFieldA | Agda.Syntax.Concrete |
| nameFixity | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| NameId | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| nameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| NameKind | Agda.Interaction.Highlighting.Precise |
| nameModifiers | Agda.Interaction.InteractionTop |
| nameOf | Agda.Syntax.Common |
| nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| nameOfFlat | Agda.TypeChecking.Monad.Builtin |
| nameOfInf | Agda.TypeChecking.Monad.Builtin |
| nameOfSharp | Agda.TypeChecking.Monad.Builtin |
| NamePart | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.TypeChecking.Unquote |
| nameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| Names | Agda.Syntax.Translation.ReflectedToAbstract |
| NamesIn | Agda.Syntax.Internal.Names |
| namesIn | Agda.Syntax.Internal.Names |
| namesInFoldable | Agda.Syntax.Internal.Names |
| NamesInScope | Agda.Syntax.Scope.Base |
| namesInScope | Agda.Syntax.Scope.Base |
| NameSpace | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base |
| nameSpaceAccess | Agda.Syntax.Scope.Base |
| NameSpaceId | Agda.Syntax.Scope.Base |
| namesToNotation | Agda.Syntax.Fixity |
| nameStringParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NameSupply | Agda.Compiler.MAlonzo.Compiler |
| nameSupply | Agda.Compiler.Epic.CompileState |
| NameTag | Agda.Syntax.Scope.Base |
| nameToArgName | Agda.Syntax.Internal |
| nameToPatVarName | Agda.Syntax.Internal |
| nameToRawName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| nameVariant | Agda.Utils.Suffix |
| Nat | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.TypeChecking.Primitive |
| 3 (Data Constructor) | Agda.TypeChecking.Primitive |
| 4 (Type/Class) | Agda.Auto.Syntax |
| nat | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| natPrimTF | Agda.Compiler.Epic.Primitive |
| NeedOptionCopatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NeedOptionRewriting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| neg | Agda.TypeChecking.Polarity |
| NegApp | Agda.Utils.Haskell.Syntax |
| Negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
| negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
| negPlusKView | Agda.Syntax.Treeless |
| negtype | Agda.Auto.Convert |
| neighbours | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| neighboursMap | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| nest | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| nestedComment | Agda.Syntax.Parser.Comments |
| NeutralArg | Agda.TypeChecking.MetaVars |
| NeutralLevel | Agda.Syntax.Internal |
| newArgsMeta | Agda.TypeChecking.MetaVars |
| newArgsMeta' | Agda.TypeChecking.MetaVars |
| newArgsMetaCtx | Agda.TypeChecking.MetaVars |
| newArgsMetaCtx' | Agda.TypeChecking.MetaVars |
| newCTree | Agda.Auto.NarrowingSearch |
| NewFlex | Agda.Utils.Warshall |
| newIFSMeta | Agda.TypeChecking.MetaVars |
| newIFSMetaCtx | Agda.TypeChecking.MetaVars |
| newInteractionMetaArg | Agda.TypeChecking.Implicit |
| newIORef | Agda.Utils.IORef |
| newLayoutContext | Agda.Syntax.Parser.Layout |
| newMeta | |
| 1 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Auto.NarrowingSearch |
| newMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| newMetaArg | Agda.TypeChecking.Implicit |
| NewModuleName | Agda.Syntax.Translation.ConcreteToAbstract |
| NewModuleQName | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract |
| NewName | Agda.Syntax.Translation.ConcreteToAbstract |
| newName | Agda.Compiler.Epic.CompileState |
| newNamedValueMeta | Agda.TypeChecking.MetaVars |
| newNamedValueMeta' | Agda.TypeChecking.MetaVars |
| NewNotation | |
| 1 (Type/Class) | Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Fixity |
| newOKHandle | Agda.Auto.NarrowingSearch |
| newPlaceholder | Agda.Auto.NarrowingSearch |
| newProblem | Agda.TypeChecking.Constraints |
| newProblem_ | Agda.TypeChecking.Constraints |
| newPtr | Agda.Utils.Pointer, Agda.Syntax.Internal |
| newQuestionMark | Agda.TypeChecking.MetaVars |
| newQuestionMark' | Agda.TypeChecking.MetaVars |
| newRecordMeta | Agda.TypeChecking.MetaVars |
| newRecordMetaCtx | Agda.TypeChecking.MetaVars |
| newSection | Agda.TypeChecking.Rules.Def |
| newSortMeta | Agda.TypeChecking.MetaVars |
| newSortMeta' | Agda.TypeChecking.MetaVars |
| newSortMetaBelowInf | Agda.TypeChecking.MetaVars |
| newSortMetaCtx | Agda.TypeChecking.MetaVars |
| newSortMetaCtx' | Agda.TypeChecking.MetaVars |
| newSubConstraints | Agda.Auto.NarrowingSearch |
| newTelMeta | Agda.TypeChecking.MetaVars |
| NewType | Agda.Utils.Haskell.Syntax |
| newTypeMeta | Agda.TypeChecking.MetaVars |
| newTypeMeta_ | Agda.TypeChecking.MetaVars |
| newValueMeta | Agda.TypeChecking.MetaVars |
| newValueMeta' | Agda.TypeChecking.MetaVars |
| newValueMetaCtx | Agda.TypeChecking.MetaVars |
| newValueMetaCtx' | Agda.TypeChecking.MetaVars |
| nextChar | Agda.Syntax.Parser.LookAhead |
| nextFresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nextFresh' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nextName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| nextNode | Agda.Utils.Warshall |
| nextPolarity | Agda.TypeChecking.Polarity |
| nextSplit | Agda.TypeChecking.CompiledClause.Compile |
| nextSuffix | Agda.Utils.Suffix |
| Nice | Agda.Syntax.Concrete.Definitions |
| NiceConstructor | Agda.Syntax.Concrete.Definitions |
| NiceDataSig | Agda.Syntax.Concrete.Definitions |
| NiceDeclaration | Agda.Syntax.Concrete.Definitions |
| niceDeclarations | Agda.Syntax.Concrete.Definitions |
| NiceField | Agda.Syntax.Concrete.Definitions |
| NiceFunClause | Agda.Syntax.Concrete.Definitions |
| niceHasAbstract | Agda.Syntax.Concrete.Definitions |
| NiceImport | Agda.Syntax.Concrete.Definitions |
| NiceModule | Agda.Syntax.Concrete.Definitions |
| NiceModuleMacro | Agda.Syntax.Concrete.Definitions |
| NiceMutual | Agda.Syntax.Concrete.Definitions |
| NiceOpen | Agda.Syntax.Concrete.Definitions |
| NicePatternSyn | Agda.Syntax.Concrete.Definitions |
| NicePragma | Agda.Syntax.Concrete.Definitions |
| NiceRecSig | Agda.Syntax.Concrete.Definitions |
| NiceTypeSignature | Agda.Syntax.Concrete.Definitions |
| NiceUnquoteDecl | Agda.Syntax.Concrete.Definitions |
| NiceUnquoteDef | Agda.Syntax.Concrete.Definitions |
| nilListT | Agda.Utils.ListT |
| NK | Agda.Syntax.Concrete.Operators.Parser |
| NLM | Agda.TypeChecking.Rewriting.NonLinMatch |
| nlmEqs | Agda.TypeChecking.Rewriting.NonLinMatch |
| NLMState | |
| 1 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
| 2 (Data Constructor) | Agda.TypeChecking.Rewriting.NonLinMatch |
| nlmSub | Agda.TypeChecking.Rewriting.NonLinMatch |
| NLPat | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NLPatVars | Agda.TypeChecking.Rewriting |
| nlPatVars | Agda.TypeChecking.Rewriting |
| NLPType | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nlpTypeLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nlpTypeUnEl | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nmEnv | Agda.Compiler.UHC.FromAgda |
| nmid | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nmSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| No | |
| 1 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| 3 (Data Constructor) | Agda.TypeChecking.InstanceArguments |
| NoAbs | Agda.Syntax.Internal |
| noabsApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| NoApp | Agda.TypeChecking.EtaContract |
| noAug | Agda.Termination.CallMatrix |
| NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noblks | Agda.Auto.Typecheck |
| noCheckCover | Agda.Compiler.MAlonzo.Primitives |
| noCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noConPatternInfo | Agda.Syntax.Internal |
| noConstraints | Agda.TypeChecking.Constraints |
| 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 |
| nodeC | Agda.TypeChecking.Serialise.Base |
| nodeD | Agda.TypeChecking.Serialise.Base |
| nodeE | Agda.TypeChecking.Serialise.Base |
| NodeFlex | Agda.TypeChecking.SizedTypes.WarshallSolver |
| nodeFromSizeExpr | Agda.TypeChecking.SizedTypes.WarshallSolver |
| NodeId | Agda.Utils.Warshall |
| NodeInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
| NodeK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| nodeMap | Agda.Utils.Warshall |
| nodeMemo | Agda.TypeChecking.Serialise.Base |
| NodeRigid | Agda.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 |
| nodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| nodeToSizeExpr | Agda.TypeChecking.SizedTypes.WarshallSolver |
| NodeZero | Agda.TypeChecking.SizedTypes.WarshallSolver |
| NoEta | Agda.TypeChecking.Datatypes |
| noFixity | Agda.Syntax.Fixity |
| noFixity' | Agda.Syntax.Fixity |
| noFunctionsIntoSize | Agda.TypeChecking.Rules.Term |
| NoFunSig | Agda.Syntax.Abstract |
| NoHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noHighlightingInRange | Agda.Interaction.Highlighting.Precise |
| NoId | Agda.Auto.Syntax |
| NoInsertNeeded | Agda.TypeChecking.Implicit |
| NoInv | Agda.TypeChecking.Injectivity |
| noiotastep | Agda.Auto.Typecheck |
| noiotastep_term | Agda.Auto.Typecheck |
| NoLayout | Agda.Syntax.Parser.Monad |
| noMatchLit | Agda.TypeChecking.Coverage.Match |
| noModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| noMsg | Agda.Utils.Except |
| noMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| Non | Agda.Syntax.Concrete.Operators.Parser |
| NoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| noName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| noName_ | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NonAssoc | Agda.Syntax.Fixity |
| NonCanonical | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| None | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NonFatalErrors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NonfixK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| NonfixNotation | Agda.Syntax.Notation |
| nonIncreasing | Agda.Termination.Order |
| NonInteractive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nonLinMatch | Agda.TypeChecking.Rewriting.NonLinMatch |
| NoNotation | Agda.Syntax.Notation |
| noNotation | Agda.Syntax.Notation |
| nonRecursiveRecord | Agda.TypeChecking.Records |
| NonStrict | Agda.Syntax.Common |
| nonStrictToIrr | Agda.Syntax.Common |
| nonStrictToRel | Agda.Syntax.Common |
| NonTerminating | Agda.Syntax.Common |
| NonTerminatingReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Nonvariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| nonvariantToUnusedArg | Agda.TypeChecking.Polarity |
| nonvariantToUnusedArgInClause | Agda.TypeChecking.Polarity |
| nonvariantToUnusedArgInDef | Agda.TypeChecking.Polarity |
| NoOccurrence | |
| 1 (Data Constructor) | Agda.TypeChecking.Free.Old |
| 2 (Data Constructor) | Agda.TypeChecking.Free |
| NoOutputTypeName | Agda.TypeChecking.Telescope |
| NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noPatternMatchingOnCodata | Agda.TypeChecking.Rules.LHS |
| NoPlaceholder | Agda.Syntax.Common |
| noPlaceholder | Agda.Syntax.Common |
| NoPositivityCheckPragma | Agda.Syntax.Concrete |
| NoPrio | Agda.Auto.NarrowingSearch |
| noProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest |
| NoProjectedVar | Agda.TypeChecking.MetaVars |
| noProjectedVar | Agda.TypeChecking.MetaVars |
| NoProjection | Agda.TypeChecking.ProjectionLike |
| NoRange | Agda.Syntax.Position |
| noRange | Agda.Syntax.Position |
| NoReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoRHSRequiresAbsurdPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| norm | Agda.Auto.Convert |
| normal | Agda.Syntax.Parser.Lexer |
| normalForm | Agda.Interaction.BasicOps |
| NormalHole | Agda.Syntax.Notation |
| Normalise | Agda.TypeChecking.Reduce |
| normalise | Agda.TypeChecking.Reduce |
| normalise' | Agda.TypeChecking.Reduce |
| normaliseB' | Agda.TypeChecking.Rewriting.NonLinMatch |
| Normalised | Agda.Interaction.BasicOps |
| NormaliseProjP | Agda.TypeChecking.Records |
| normaliseProjP | Agda.TypeChecking.Records, Agda.TypeChecking.Coverage |
| normaliseStatic | Agda.Compiler.Epic.Static |
| normalizeNames | Agda.Compiler.Treeless.NormalizeNames |
| normalMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noSection | Agda.Syntax.Fixity |
| noShadowingOfConstructors | Agda.TypeChecking.Rules.LHS |
| NoSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuchBuiltinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuchName | Agda.TypeChecking.Implicit |
| NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuffix | Agda.Utils.Suffix |
| not' | Agda.Syntax.Parser.Alex |
| NotADatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notaFixity | Agda.Syntax.Fixity |
| notAHaskellType | Agda.Compiler.HaskellTypes |
| notaIsOperator | Agda.Syntax.Fixity |
| noTakenNames | Agda.Syntax.Translation.AbstractToConcrete |
| NotAllowedInMutual | Agda.Syntax.Concrete.Definitions |
| NotAModuleExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notaName | Agda.Syntax.Fixity |
| notaNames | Agda.Syntax.Fixity |
| NotAnExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotAProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Notation | Agda.Syntax.Notation |
| notation | Agda.Syntax.Fixity |
| NotationKind | Agda.Syntax.Notation |
| notationKind | Agda.Syntax.Notation |
| notationNames | Agda.Syntax.Fixity |
| NotationSection | |
| 1 (Type/Class) | Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Fixity |
| NotAValidLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotB | Agda.Auto.NarrowingSearch |
| NotBlocked | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Internal |
| notBlocked | Agda.Syntax.Internal |
| NotComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| NotDelayed | Agda.Syntax.Common |
| notDominated | Agda.Utils.Favorites |
| note | Agda.Interaction.Highlighting.Precise |
| notequal | Agda.Auto.CaseSplit |
| NoTerminationCheck | Agda.Syntax.Common |
| NotForced | Agda.Compiler.Epic.Interface |
| notForced | Agda.Compiler.Epic.Interface |
| NotFound | Agda.Interaction.FindFile |
| NotHidden | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| notHidden | Agda.Syntax.Common |
| Nothing | |
| 1 (Data Constructor) | Agda.Utils.Maybe |
| 2 (Data Constructor) | Agda.Utils.Maybe.Strict |
| NothingAppliedToHiddenArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NothingAppliedToInstanceArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NothingToPrune | Agda.TypeChecking.MetaVars.Occurs |
| nothingToSplitError | Agda.TypeChecking.Rules.LHS.Instantiate |
| NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotInductive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notInScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| notInScopeName | Agda.Syntax.Internal |
| NotInstanceDef | Agda.Syntax.Common |
| NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotM | Agda.Auto.NarrowingSearch |
| NotMacroDef | Agda.Syntax.Common |
| NotMain | Agda.Compiler.Common |
| NotMainInterface | Agda.Interaction.Imports |
| notMasked | Agda.Termination.Monad |
| notMember | Agda.Utils.Bag |
| NotPB | Agda.Auto.NarrowingSearch |
| notPlaceholder | Agda.Syntax.Concrete.Operators.Parser |
| NotReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notShadowedLocal | Agda.Syntax.Scope.Base |
| notShadowedLocals | Agda.Syntax.Scope.Base |
| notSoNiceDeclarations | Agda.Syntax.Concrete.Definitions |
| NotStrictlyPositive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotValidBeforeField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notVisible | Agda.Syntax.Common |
| NotWorse | Agda.Termination.Order |
| notWorse | Agda.Termination.Order |
| NoUnfold | Agda.TypeChecking.MetaVars.Occurs |
| NoUnify | Agda.TypeChecking.Rules.LHS.Unify |
| NoWarnings | Agda.Interaction.Imports |
| NoWhere | Agda.Syntax.Concrete |
| NoWithFunction | Agda.TypeChecking.Rules.Def |
| nowSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| nPi | Agda.TypeChecking.Primitive |
| nrBinds | Agda.Compiler.Epic.Injection |
| nrRel | Agda.Compiler.Epic.NatDetection |
| nsInScope | Agda.Syntax.Scope.Base |
| nsModules | Agda.Syntax.Scope.Base |
| nsNames | Agda.Syntax.Scope.Base |
| nubOn | Agda.Utils.List |
| Null | Agda.Utils.Null |
| null | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.HashMap |
| 3 (Function) | Agda.Utils.Bag |
| 4 (Function) | Agda.Utils.Null |
| Number | Agda.Interaction.Highlighting.Precise |
| numberPatVars | Agda.Syntax.Internal.Pattern |
| NumHoles | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| numHoles | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |