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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- $
- %
- +
- .
- /
- <
- =
- >
- ^
- -
- _
- All

Index - N

Name |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
4 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
5 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
6 (Data Constructor) | Agda.Interaction.Highlighting.Precise
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.Common
namedArgName | Agda.Syntax.Internal
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
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, 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
nameModifiers | Agda.Interaction.InteractionTop
nameNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameOf | Agda.Syntax.Common
nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfFlat | Agda.TypeChecking.Monad.Builtin
nameOfHComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nameOfInf | Agda.TypeChecking.Monad.Builtin
nameOfSharp | Agda.TypeChecking.Monad.Builtin
nameOfTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Translation.ReflectedToAbstract
2 (Type/Class) | Agda.TypeChecking.Names
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.Fixity
nameStringParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NameSupply | Agda.Compiler.MAlonzo.Compiler
NameTag | Agda.Syntax.Scope.Base
nameToArgName | Agda.Syntax.Internal
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
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
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.Fixity
2 (Data Constructor) | Agda.Syntax.Fixity
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
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
NLPatVars | Agda.TypeChecking.Rewriting
nlPatVars | Agda.TypeChecking.Rewriting
nlPatVarsUnder | Agda.TypeChecking.Rewriting
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
nlpTypeLevel | 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
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
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
NoEta | Agda.Syntax.Common
noFixity | Agda.Syntax.Fixity
noFixity' | Agda.Syntax.Fixity
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
NoLayout | Agda.Syntax.Parser.Monad
NoMetadata | Agda.Syntax.Scope.Base
noMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Fixity
NonCanonical | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
None | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonemptyList | Agda.Utils.NonemptyList
NonFatalErrors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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, Agda.Compiler.Backend
Nonvariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoOccurrence |
1 (Data Constructor) | Agda.TypeChecking.Free
2 (Data Constructor) | Agda.TypeChecking.Free.Old
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
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.Notation
Normalise | Agda.TypeChecking.Reduce
normalise | Agda.TypeChecking.Reduce
normalise' | Agda.TypeChecking.Reduce
normaliseB | Agda.TypeChecking.Reduce
Normalised | Agda.Interaction.BasicOps
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.Fixity
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.Fixity
notaIsOperator | Agda.Syntax.Fixity
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.Fixity
notaNames | Agda.Syntax.Fixity
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.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, 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
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
notInScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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 | Agda.Utils.Bag
NotOnlyTokenBased | Agda.Interaction.Highlighting.Precise
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
NoWarn | Agda.Syntax.Concrete.Fixity
NoWarnings | Agda.Interaction.Imports
noWarnings | Agda.Interaction.Options.Warnings
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
nPi' | 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.HashMap
3 (Function) | Agda.Utils.Bag
4 (Function) | Agda.Utils.Null
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