Agda-2.8.0: 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

NakedUnquote | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NakedUnquote_ | Agda.Interaction.Options.Errors
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
nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
nameC | Agda.TypeChecking.Serialise.Base
nameCanonical | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
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
namedBindsToTel1 | 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.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
namedMetaOf | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop
NamedName | Agda.Syntax.Common
NamedRecCon | Agda.Syntax.Abstract
NamedRigid |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
namedSame | Agda.Syntax.Common
namedTelVars | Agda.TypeChecking.Substitute
namedThing | Agda.Syntax.Common
namedVarP | Agda.Syntax.Internal
NamedWhereModuleInRefinedContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NamedWhereModuleInRefinedContext_ | Agda.Interaction.Options.Errors
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 |
1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Type/Class) | Agda.Compiler.MAlonzo.Misc
NameKinds | Agda.Interaction.Highlighting.FromAbstract
NameMap | Agda.Syntax.Scope.Base
NameMapEntry |
1 (Type/Class) | Agda.Syntax.Scope.Base
2 (Data Constructor) | 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, Agda.Syntax.Common
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
nameOfUniv | Agda.TypeChecking.Monad.Builtin, 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
nameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameRange | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NameResolutionError | Agda.Syntax.Scope.Base
nameRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Names | Agda.TypeChecking.Names
namesAndMetasIn | Agda.Syntax.Internal.Names
namesAndMetasIn' | Agda.Syntax.Internal.Names
NamesIn | Agda.Syntax.Internal.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.Notation
nameStringParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSuffix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSuffixView | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
NAPs1 | Agda.Syntax.Abstract
Nat |
1 (Type/Class) | Agda.Syntax.Common
2 (Type/Class) | Agda.TypeChecking.Primitive
3 (Data Constructor) | Agda.TypeChecking.Primitive
nat | Agda.Compiler.Treeless.EliminateLiteralPatterns
Nat1 | Agda.Syntax.Common
natSize | Agda.Utils.Size
NeedOptionAllowExec | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionAllowExec_ | Agda.Interaction.Options.Errors
NeedOptionCopatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionCopatterns_ | Agda.Interaction.Options.Errors
NeedOptionCubical | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionCubical_ | Agda.Interaction.Options.Errors
NeedOptionPatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionPatternMatching_ | Agda.Interaction.Options.Errors
NeedOptionProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionProp_ | Agda.Interaction.Options.Errors
NeedOptionRewriting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionRewriting_ | Agda.Interaction.Options.Errors
NeedOptionSizedTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionSizedTypes_ | Agda.Interaction.Options.Errors
NeedOptionTwoLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionTwoLevel_ | Agda.Interaction.Options.Errors
NeedOptionUniversePolymorphism | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NeedOptionUniversePolymorphism_ | Agda.Interaction.Options.Errors
NegApp | Agda.Utils.Haskell.Syntax
Negative |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver
negative | Agda.TypeChecking.SizedTypes.WarshallSolver
NegativeLiteralInPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NegativeLiteralInPattern_ | Agda.Interaction.Options.Errors
negativePolarity | Agda.Syntax.Common
NegativeUnification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
negativeUnificationErrorNameString | Agda.Interaction.Options.Errors
NegativeUnification_ | Agda.Interaction.Options.Errors
negPlusKView | Agda.Syntax.Treeless, Agda.Compiler.Backend
neighbours | Agda.Utils.Graph.AdjacencyMap.Unidirectional
neighboursMap | Agda.Utils.Graph.AdjacencyMap.Unidirectional
NEMap | Agda.Utils.Map1
NESet | Agda.Utils.Set1
nest |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
nestedComment | Agda.Syntax.Parser.Comments
NeutralArg | Agda.TypeChecking.MetaVars
NeverColour | Agda.Interaction.Options
NeverProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
neverUnblock | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
newArgsMeta | Agda.TypeChecking.MetaVars
newArgsMeta' | Agda.TypeChecking.MetaVars
newArgsMetaCtx | Agda.TypeChecking.MetaVars
newArgsMetaCtx' | Agda.TypeChecking.MetaVars
newArgsMetaCtx'' | Agda.TypeChecking.MetaVars
newInstanceMeta | Agda.TypeChecking.MetaVars
newInstanceMetaCtx | Agda.TypeChecking.MetaVars
newInteractionMetaArg | Agda.TypeChecking.Implicit
newIORef | Agda.Utils.IORef
newLayoutBlock | Agda.Syntax.Parser.Layout
newLevelMeta | Agda.TypeChecking.MetaVars
newMeta | 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
newNamedValueMeta | Agda.TypeChecking.MetaVars
newNamedValueMeta' | Agda.TypeChecking.MetaVars
NewNotation |
1 (Type/Class) | Agda.Syntax.Notation
2 (Data Constructor) | Agda.Syntax.Notation
newOptionName | Agda.Interaction.Options
newProblem | Agda.TypeChecking.Constraints
newProblem_ | Agda.TypeChecking.Constraints
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
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
newValueMetaOfKind | Agda.TypeChecking.MetaVars
nextChar | Agda.Syntax.Parser.LookAhead
nextFileId | Agda.Utils.FileId
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
nextLocalMeta | Agda.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
nextNameId | Agda.Syntax.Concrete.Definitions.Monad
nextPolarity | Agda.TypeChecking.Polarity
nextRawName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nextSplit | Agda.TypeChecking.CompiledClause.Compile
nextSuffix | Agda.Utils.Suffix
Nice |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Monad
NiceConstructor | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceDataDef | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceDataSig | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceDeclaration | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
niceDeclarations | Agda.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
NiceField | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceFunClause | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceGeneralize | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
niceHasAbstract | Agda.Syntax.Concrete.Definitions
NiceImport | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceLoneConstructor | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceModule | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceModuleMacro | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceMutual | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceOpaque | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceOpen | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NicePatternSyn | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NicePragma | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceRecDef | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceRecSig | Agda.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
NiceTypeSignature | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceUnquoteData | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceUnquoteDecl | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
NiceUnquoteDef | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
niceWarn | Agda.Syntax.Concrete.Definitions.Monad
niceWarning | Agda.Syntax.Concrete.Definitions.Monad
NiceWarnings | Agda.Syntax.Concrete.Definitions.Monad
NicifierError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NicifierError_ | Agda.Interaction.Options.Errors
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 |
1 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor) | 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.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nmSuggestion | Agda.TypeChecking.Monad.Base.Types, 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
NoActionForInteractionPoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoActionForInteractionPoint_ | Agda.Interaction.Options.Errors
NoApp | Agda.TypeChecking.EtaContract
NoArg | Agda.Utils.GetOpt, Agda.Interaction.Options
noAug | Agda.Termination.CallMatrix
NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoBindingForBuiltin_ | Agda.Interaction.Options.Errors
NoBindingForPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoBindingForPrimitive_ | Agda.Interaction.Options.Errors
NoCatchall | Agda.Syntax.Common
noCheckCover | Agda.Compiler.MAlonzo.Primitives
noCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
noConPatternInfo | Agda.Syntax.Internal
noConstraints | Agda.TypeChecking.Constraints
noConstraints' | Agda.TypeChecking.Constraints
NoCoverageCheck | Agda.Syntax.Common
NoCoverageCheckPragma | Agda.Syntax.Concrete
NoCubical | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
noDataDefParams | Agda.Syntax.Abstract
Node |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Type/Class) | Agda.TypeChecking.Serialise.Base
3 (Type/Class) | Agda.TypeChecking.Positivity
4 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver
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
NodeInfty | Agda.TypeChecking.SizedTypes.WarshallSolver
NodeK | Agda.Syntax.Concrete.Operators.Parser.Monad
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
NoDisplayLHS | Agda.Syntax.Common
noDotOrEqPattern | Agda.Syntax.Abstract.Pattern
NoEllipsis | Agda.Syntax.Common
NoErasedMatches | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoEta | Agda.Syntax.Common
noFixity | Agda.Syntax.Common
noFixity' | Agda.Syntax.Common
noFreeVariables | Agda.Syntax.Common
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
NoHints | Agda.Mimer.Options
NoInfo | Agda.TypeChecking.Coverage.SplitClause
NoInsertNeeded | Agda.TypeChecking.Implicit
NoInv | Agda.TypeChecking.Injectivity
NoK | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoKnownRecordWithSuchFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoKnownRecordWithSuchFields_ | Agda.Interaction.Options.Errors
nolam | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
NoLeftInv | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
noLoneSigs | Agda.Syntax.Concrete.Definitions.Monad
NoMain | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoMain_ | Agda.Interaction.Options.Warnings
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
noModuleNameHash | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
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
NonCanonical_ | Agda.Interaction.Options.Errors
nonConstraining | Agda.TypeChecking.Constraints
None | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonEmpty | Agda.Utils.List1
nonEmpty | Agda.Utils.List1
nonEmptyMap | Agda.Utils.Map1
nonEmptySet | Agda.Utils.Set1
NonFatalErrors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
nonFatalErrors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Warnings, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonFatalErrors_ | Agda.Interaction.Options.Errors
NonfixK | Agda.Syntax.Concrete.Operators.Parser.Monad
NonfixNotation | Agda.Syntax.Notation
nonIncreasing | Agda.Termination.Order
NonInteractive | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NonLazy | Agda.TypeChecking.Patterns.Match
nonLinMatch | Agda.TypeChecking.Rewriting.NonLinMatch
NoNoError | Agda.Interaction.Options.Warnings
NoNotation | Agda.Syntax.Notation
noNotation | Agda.Syntax.Common
nonRecursiveRecord | Agda.TypeChecking.Records
NonTerminating | Agda.Syntax.Common
NonTerminatingReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Nonvariant | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoOpaque | Agda.Syntax.Common
NoOutputTypeName | Agda.TypeChecking.InstanceArguments
NoOverlap | Agda.Syntax.Common
NoParameterOfName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoParameterOfName_ | Agda.Interaction.Options.Errors
NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoParseForApplication_ | Agda.Interaction.Options.Errors
NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoParseForLHS_ | Agda.Interaction.Options.Errors
NoPlaceholder | Agda.Syntax.Common
noPlaceholder | Agda.Syntax.Common
NoPositivityCheck | Agda.Syntax.Common
NoPositivityCheckPragma | Agda.Syntax.Concrete
NoPostfix | Agda.TypeChecking.ProjectionLike
NoPragmaFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoPragmaFor_ | Agda.Interaction.Options.Errors
noProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest
noProfileOptions | Agda.Utils.ProfileOptions
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
normal | Agda.Syntax.Parser.Lexer
normalForm | Agda.Interaction.BasicOps
Normalise | Agda.TypeChecking.Reduce
normalise | Agda.TypeChecking.Reduce
normalise' | Agda.TypeChecking.Reduce
Normalised | Agda.Interaction.Base
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
NoSubst |
1 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
2 (Data Constructor) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
NoSuchBuiltinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchBuiltinName_ | Agda.Interaction.Options.Errors
NoSuchInteractionPoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchInteractionPoint_ | Agda.Interaction.Options.Errors
NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchModule_ | Agda.Interaction.Options.Errors
NoSuchName | Agda.TypeChecking.Implicit
NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoSuchPrimitiveFunction_ | Agda.Interaction.Options.Errors
NoSuffix | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
not | Agda.Utils.Boolean
not' | Agda.Syntax.Parser.Alex
NotADatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotADatatype_ | Agda.Interaction.Options.Errors
NotAffectedByOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotAffectedByOpaque_ | Agda.Interaction.Options.Warnings
notaFixity | Agda.Syntax.Notation
NotAHaskellType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notAHaskellTypeErrorName | Agda.TypeChecking.Errors.Names
notAHaskellTypeErrorNameString | Agda.Interaction.Options.Errors
NotAHaskellType_ |
1 (Type/Class) | Agda.Interaction.Options.Errors
2 (Data Constructor) | Agda.Interaction.Options.Errors
notaIsOperator | Agda.Syntax.Notation
noTakenNames | Agda.Syntax.Translation.AbstractToConcrete
NotAllowedInDotPatterns |
1 (Type/Class) | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notAllowedInDotPatternsString | Agda.Interaction.Options.Errors
NotAllowedInDotPatterns_ | Agda.Interaction.Options.Errors
NotAllowedInMutual | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
NotAllowedInMutual_ | Agda.Interaction.Options.Warnings
NotAmbiguous | 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
NotAnExpression_ | Agda.Interaction.Options.Errors
NotARewriteRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotARewriteRule_ | Agda.Interaction.Options.Warnings
Notation | Agda.Syntax.Common
notation | Agda.Syntax.Notation
NotationKind | Agda.Syntax.Notation
notationKind | Agda.Syntax.Notation
notationNames | Agda.Syntax.Notation
NotationPart | Agda.Syntax.Common
NotationSection |
1 (Type/Class) | Agda.Syntax.Notation
2 (Data Constructor) | Agda.Syntax.Notation
NotAValidLetBinding |
1 (Type/Class) | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notAValidLetBindingString | Agda.Interaction.Options.Errors
NotAValidLetBinding_ | Agda.Interaction.Options.Errors
NotAValidLetExpression |
1 (Type/Class) | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
notAValidLetExpressionString | Agda.Interaction.Options.Errors
NotAValidLetExpression_ | Agda.Interaction.Options.Errors
NotAValidLetPattern | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotBlocked |
1 (Data Constructor) | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
2 (Type/Class) | Agda.Syntax.Internal
notBlocked | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
NotBlocked' | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
NotBlockedOnResult | Agda.TypeChecking.Coverage.Match
notBlocked_ | Agda.Syntax.Internal.Blockers, 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
NotCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotCompiled_ | Agda.Interaction.Options.Errors
notDominated | Agda.Utils.Favorites
note | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
NotErased | Agda.Syntax.Common
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
NothingToPrune | Agda.TypeChecking.MetaVars.Occurs
NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotImplemented_ | Agda.Interaction.Options.Errors
NotInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotInMutual | Agda.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
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_ |
1 (Data Constructor) | Agda.Interaction.Options.Warnings
2 (Data Constructor) | Agda.Interaction.Options.Errors
NotInstanceDef | Agda.Syntax.Common
NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotLeqSort_ | Agda.Interaction.Options.Errors
NotMacroDef | Agda.Syntax.Common
NotMain | Agda.Syntax.Common, Agda.Compiler.Common, Agda.Compiler.Backend
notMasked | Agda.Termination.Monad
notMember |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.Bag
4 (Function) | Agda.Utils.BoolSet
5 (Function) | Agda.Utils.SmallSet
NotOnlyTokenBased | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
NotOverapplied | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotProjectionLikePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
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
notSoPrettySigCubicalNotErasure | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
NotSupported_ | Agda.Interaction.Options.Errors
notUnderOpaque | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotValidBeforeField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NotValidBeforeField_ | Agda.Interaction.Options.Errors
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
NoUnused | Agda.Compiler.MAlonzo.Misc
noUserQuantity | Agda.Syntax.Common
NoWarn | Agda.Syntax.Concrete.Fixity
noWarnings | Agda.Interaction.Options.Warnings
nowDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
NoWhere | Agda.Syntax.Concrete
noWhereDecls | Agda.Syntax.Abstract
NoWhere_ | Agda.Syntax.Concrete
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
nub | Agda.Utils.List1
nubAndDuplicatesOn | Agda.Utils.List
nubBy | Agda.Utils.List1
nubFavouriteOn | Agda.Utils.List
nubM |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
nubOn | Agda.Utils.List
Null |
1 (Data Constructor) | Agda.Interaction.JSON
2 (Type/Class) | Agda.Utils.Null
3 (Data Constructor) | Agda.Compiler.JS.Syntax
null |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Bag
3 (Function) | Agda.Utils.BoolSet
4 (Function) | Agda.Utils.Null
5 (Function) | Agda.Utils.SmallSet
Number |
1 (Data Constructor) | Agda.Interaction.JSON
2 (Data Constructor) | Agda.Syntax.Common.Aspect, 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