| 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 |
| nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| nameC | Agda.TypeChecking.Serialise.Base |
| nameConcrete | Agda.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 |
| nameD | Agda.TypeChecking.Serialise.Base |
| named | Agda.Syntax.Common |
| NamedArg | Agda.Syntax.Common |
| namedArg | Agda.Syntax.Common |
| namedArgFromDom | Agda.Syntax.Internal |
| namedArgName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| NamedArgs | Agda.Syntax.Internal |
| NamedBinding | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Pretty |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Pretty |
| namedBinding | Agda.Syntax.Concrete.Pretty |
| namedBindsToTel | Agda.TypeChecking.Substitute |
| NamedClause | |
| 1 (Type/Class) | Agda.Syntax.Translation.InternalToAbstract |
| 2 (Data Constructor) | Agda.Syntax.Translation.InternalToAbstract |
| namedClausePats | Agda.Syntax.Internal |
| namedDBVarP | Agda.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 |
| namedMetaOf | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop |
| NamedName | Agda.Syntax.Common |
| NamedRigid | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Solve |
| namedSame | Agda.Syntax.Common |
| namedTelVars | Agda.TypeChecking.Substitute |
| namedThing | Agda.Syntax.Common |
| namedVarP | Agda.Syntax.Internal |
| Named_ | Agda.Syntax.Common |
| nameFieldA | Agda.Syntax.Concrete |
| nameFixity | Agda.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 |
| NameInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| nameInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| nameIsRecordName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| NameKind | Agda.Interaction.Highlighting.Precise |
| NameMap | Agda.Syntax.Scope.Base |
| NameMetadata | Agda.Syntax.Scope.Base |
| nameNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NameNotModule | Agda.Syntax.Scope.Base |
| nameOf | Agda.Syntax.Common |
| nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nameOfBV' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nameOfFlat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nameOfHComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nameOfInf | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nameOfSharp | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nameOfTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NameOrModule | Agda.Syntax.Scope.Base |
| 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 |
| nameRange | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| nameRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| Names | |
| 1 (Type/Class) | Agda.TypeChecking.Names |
| 2 (Type/Class) | Agda.Syntax.Translation.ReflectedToAbstract |
| NamesIn | Agda.Syntax.Internal.Names |
| namesIn | 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 |
| NamesT | |
| 1 (Type/Class) | Agda.TypeChecking.Names |
| 2 (Data Constructor) | Agda.TypeChecking.Names |
| namesToNotation | Agda.Syntax.Notation |
| nameStringParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NameSupply | Agda.Compiler.MAlonzo.Compiler |
| NameTag | Agda.Syntax.Scope.Base |
| nameToArgName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| NameToExpr | Agda.Syntax.Abstract |
| nameToExpr | Agda.Syntax.Abstract |
| nameToPatVarName | Agda.Syntax.Internal |
| nameToRawName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NAP | Agda.Syntax.Abstract.Pattern |
| NAPs | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| Nat | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Auto.Syntax |
| 3 (Type/Class) | Agda.TypeChecking.Primitive |
| 4 (Data Constructor) | Agda.TypeChecking.Primitive |
| nat | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| NeedOptionCopatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NeedOptionProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NeedOptionRewriting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| neg | Agda.TypeChecking.Polarity |
| NegApp | Agda.Utils.Haskell.Syntax |
| Negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
| negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
| NegativeUnification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| negPlusKView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 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 |
| newAbs | Agda.Auto.SearchControl |
| newApp | Agda.Auto.SearchControl |
| newApp' | Agda.Auto.SearchControl |
| newArgs | Agda.Auto.SearchControl |
| newArgs' | Agda.Auto.SearchControl |
| newArgsMeta | Agda.TypeChecking.MetaVars |
| newArgsMeta' | Agda.TypeChecking.MetaVars |
| newArgsMetaCtx | Agda.TypeChecking.MetaVars |
| newArgsMetaCtx' | Agda.TypeChecking.MetaVars |
| newCTree | Agda.Auto.NarrowingSearch |
| NewFlex | Agda.Utils.Warshall |
| newInstanceMeta | Agda.TypeChecking.MetaVars |
| newInstanceMetaCtx | Agda.TypeChecking.MetaVars |
| newInteractionMetaArg | Agda.TypeChecking.Implicit |
| newIORef | Agda.Utils.IORef |
| newLam | Agda.Auto.SearchControl |
| newLayoutContext | Agda.Syntax.Parser.Layout |
| newLevelMeta | Agda.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 |
| newMetaArg | Agda.TypeChecking.Implicit |
| newMetaTCM' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| newNamedValueMeta | Agda.TypeChecking.MetaVars |
| newNamedValueMeta' | Agda.TypeChecking.MetaVars |
| NewNotation | |
| 1 (Type/Class) | Agda.Syntax.Notation |
| 2 (Data Constructor) | Agda.Syntax.Notation |
| newOKHandle | Agda.Auto.NarrowingSearch |
| newPi | Agda.Auto.SearchControl |
| newPlaceholder | Agda.Auto.NarrowingSearch |
| newProblem | Agda.TypeChecking.Constraints |
| newProblem_ | Agda.TypeChecking.Constraints |
| newPtr | Agda.Utils.Pointer |
| 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 |
| newSortMetaBelowInf | 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 |
| 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, Agda.Compiler.Backend |
| nextFresh' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nextHole | Agda.Utils.Zipper |
| nextIsForced | Agda.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 |
| nextNode | Agda.Utils.Warshall |
| nextPolarity | Agda.TypeChecking.Polarity |
| nextSplit | Agda.TypeChecking.CompiledClause.Compile |
| nextStr | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| nextSuffix | Agda.Utils.Suffix |
| Nice | Agda.Syntax.Concrete.Definitions |
| NiceConstructor | Agda.Syntax.Concrete.Definitions |
| NiceDataDef | 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 |
| NiceGeneralize | 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 |
| NiceRecDef | Agda.Syntax.Concrete.Definitions |
| NiceRecSig | Agda.Syntax.Concrete.Definitions |
| NiceTypeSignature | Agda.Syntax.Concrete.Definitions |
| NiceUnquoteDecl | Agda.Syntax.Concrete.Definitions |
| NiceUnquoteDef | Agda.Syntax.Concrete.Definitions |
| NicifierIssue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Nil | Agda.Utils.IndexedList |
| 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, Agda.Compiler.Backend |
| NLPatToTerm | Agda.TypeChecking.Rewriting.NonLinPattern |
| nlPatToTerm | Agda.TypeChecking.Rewriting.NonLinPattern |
| NLPatVars | Agda.TypeChecking.Rewriting.NonLinPattern |
| nlPatVars | Agda.TypeChecking.Rewriting.NonLinPattern |
| nlPatVarsUnder | Agda.TypeChecking.Rewriting.NonLinPattern |
| NLPSort | Agda.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 |
| nlpTypeSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nlpTypeUnEl | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nmid | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nmSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| No | |
| 1 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
| NoAbs | Agda.Syntax.Internal |
| noabsApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| NoApp | Agda.TypeChecking.EtaContract |
| noApplication | Agda.Compiler.MAlonzo.Compiler |
| NoArg | Agda.Interaction.Options |
| noAug | Agda.Termination.CallMatrix |
| NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| noblks | Agda.Auto.Typecheck |
| noCheckCover | Agda.Compiler.MAlonzo.Primitives |
| noCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| noConPatternInfo | Agda.Syntax.Internal |
| noConstraints | Agda.TypeChecking.Constraints |
| NoCoverageCheck | Agda.Syntax.Common |
| NoCoverageCheckPragma | Agda.Syntax.Concrete |
| noDataDefParams | Agda.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 |
| 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 |
| NoEllipsis | Agda.Syntax.Common |
| NoEta | Agda.Syntax.Common |
| noFixity | Agda.Syntax.Common |
| noFixity' | Agda.Syntax.Common |
| noFreeVariables | Agda.Syntax.Common |
| noFunctionsIntoSize | Agda.TypeChecking.Rules.Term |
| NoFunSig | Agda.Syntax.Abstract |
| NoGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoGeneralize | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| noGeneralizedVarsIfLetOpen | Agda.Syntax.Scope.Monad |
| NoHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| nolam | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| NoLayout | Agda.Syntax.Parser.Monad |
| NoMetadata | Agda.Syntax.Scope.Base |
| noMetas | Agda.Syntax.Internal.MetaVars |
| noModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| noMsg | Agda.Utils.Except |
| noMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Common |
| NonCanonical | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| None | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NonFatalErrors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nonFatalErrors | Agda.TypeChecking.Warnings |
| NonfixK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| NonfixNotation | Agda.Syntax.Notation |
| nonIncreasing | Agda.Termination.Order |
| NonInteractive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nonLinMatch | Agda.TypeChecking.Rewriting.NonLinMatch |
| NoNotation | Agda.Syntax.Notation |
| noNotation | Agda.Syntax.Common |
| 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, Agda.Compiler.Backend |
| Nonvariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoOutputTypeName | Agda.TypeChecking.Telescope |
| NoOverlap | Agda.Syntax.Common |
| NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoPlaceholder | Agda.Syntax.Common |
| noPlaceholder | Agda.Syntax.Common |
| NoPositivityCheck | 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, Agda.Compiler.Backend |
| NoRHSRequiresAbsurdPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| normal | Agda.Syntax.Parser.Lexer |
| normalForm | Agda.Interaction.BasicOps |
| NormalHole | Agda.Syntax.Common |
| Normalise | Agda.TypeChecking.Reduce |
| normalise | Agda.TypeChecking.Reduce |
| normalise' | Agda.TypeChecking.Reduce |
| normaliseB | Agda.TypeChecking.Reduce |
| Normalised | Agda.Interaction.Base |
| normaliseNaN | Agda.Utils.Float |
| NormaliseProjP | Agda.TypeChecking.Records |
| normaliseProjP | Agda.TypeChecking.Records, Agda.TypeChecking.Coverage |
| normalizeNames | Agda.Compiler.Treeless.NormalizeNames |
| normalMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| noSection | Agda.Syntax.Notation |
| NoSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoSuchBuiltinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoSuchName | Agda.TypeChecking.Implicit |
| NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoSuffix | Agda.Utils.Suffix |
| not' | Agda.Syntax.Parser.Alex |
| NotADatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notaFixity | Agda.Syntax.Notation |
| notaIsOperator | Agda.Syntax.Notation |
| noTakenNames | Agda.Syntax.Translation.AbstractToConcrete |
| NotAllowedInMutual | Agda.Syntax.Concrete.Definitions |
| NotAllowedInMutual_ | Agda.Interaction.Options.Warnings |
| NotAModuleExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notaName | Agda.Syntax.Notation |
| notaNames | Agda.Syntax.Notation |
| NotAnExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotAProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Notation | Agda.Syntax.Common |
| notation | Agda.Syntax.Notation |
| NotationKind | Agda.Syntax.Notation |
| notationKind | Agda.Syntax.Notation |
| notationNames | Agda.Syntax.Notation |
| NotationSection | |
| 1 (Type/Class) | Agda.Syntax.Notation |
| 2 (Data Constructor) | Agda.Syntax.Notation |
| NotAValidLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotB | Agda.Auto.NarrowingSearch |
| NotBlocked | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Internal |
| notBlocked | Agda.Syntax.Internal |
| NotBlockedOnResult | Agda.TypeChecking.Coverage.Match |
| notBlocked_ | Agda.Syntax.Internal |
| NotCheckedTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotDelayed | Agda.Syntax.Common |
| notDominated | Agda.Utils.Favorites |
| note | Agda.Interaction.Highlighting.Precise |
| notequal | Agda.Auto.CaseSplit |
| notequal' | Agda.Auto.CaseSplit |
| NoTerminationCheck | Agda.Syntax.Common |
| NotForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotFound | Agda.Interaction.FindFile |
| NotFree | Agda.TypeChecking.Free.Reduce |
| 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, Agda.Compiler.Backend |
| NothingAppliedToInstanceArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NothingToPrune | Agda.TypeChecking.MetaVars.Occurs |
| NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotInScope | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notInScopeError | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotInScopeW | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notInScopeWarning | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotInScope_ | Agda.Interaction.Options.Warnings |
| NotInstanceDef | Agda.Syntax.Common |
| NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotM | Agda.Auto.NarrowingSearch |
| NotMacroDef | Agda.Syntax.Common |
| NotMain | Agda.Compiler.Common, Agda.Compiler.Backend |
| NotMainInterface | Agda.Interaction.Imports |
| notMasked | Agda.Termination.Monad |
| notMember | |
| 1 (Function) | Agda.Utils.Bag |
| 2 (Function) | Agda.Utils.SmallSet |
| NotOnlyTokenBased | Agda.Interaction.Highlighting.Precise |
| NotOverapplied | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotPB | Agda.Auto.NarrowingSearch |
| NotReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notShadowedLocal | Agda.Syntax.Scope.Base |
| notShadowedLocals | Agda.Syntax.Scope.Base |
| notSoNiceDeclarations | Agda.Syntax.Concrete.Definitions |
| NotStrictlyPositive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotStrictlyPositive_ | Agda.Interaction.Options.Warnings |
| NotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NotValidBeforeField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| notVisible | Agda.Syntax.Common |
| NotWorse | Agda.Termination.Order |
| notWorse | Agda.Termination.Order |
| NoUnfold | Agda.TypeChecking.MetaVars.Occurs |
| NoUnify | Agda.TypeChecking.Rules.LHS.Unify |
| NoUniverseCheck | Agda.Syntax.Common |
| NoUniverseCheckPragma | Agda.Syntax.Concrete |
| noUserQuantity | Agda.Syntax.Common |
| NoWarn | Agda.Syntax.Concrete.Fixity |
| NoWarnings | Agda.Interaction.Imports |
| noWarnings | Agda.Interaction.Options.Warnings |
| nowDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NoWhere | Agda.Syntax.Concrete |
| noWhereDecls | Agda.Syntax.Abstract |
| NoWithFunction | Agda.TypeChecking.Rules.Def |
| nowSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| nPi | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| nPi' | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| 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.Bag |
| 3 (Function) | Agda.Utils.Null |
| 4 (Function) | Agda.Utils.SmallSet |
| Number | Agda.Interaction.Highlighting.Precise |
| numberOfWithPatterns | Agda.Syntax.Concrete.Pattern |
| numberPatVars | Agda.Syntax.Internal.Pattern |
| NumGeneralizableArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| NumHoles | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| numHoles | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |