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

Index - N

Name 
1 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
5 (Data Constructor)Agda.Interaction.Highlighting.Precise
nameBindingSiteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nameConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
Named 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
namedAgda.Syntax.Common
NamedArgAgda.Syntax.Common
NamedClause 
1 (Type/Class)Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
namedThingAgda.Syntax.Common
nameFixityAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nameFreqAgda.TypeChecking.Test.Generators
NameFreqs 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
nameFreqsAgda.TypeChecking.Test.Generators
NameId 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
nameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
NameKindAgda.Interaction.Highlighting.Precise
nameModifiersAgda.Interaction.GhciTop
nameOfAgda.Syntax.Common
nameOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
NamePartAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
namePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NamesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
namesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpace 
1 (Type/Class)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpaceIdAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Nat 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Common
3 (Type/Class)Agda.TypeChecking.Primitive
4 (Data Constructor)Agda.TypeChecking.Primitive
naturalAgda.Utils.TestHelpers
negAgda.TypeChecking.Polarity
NegativeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
neighboursAgda.Utils.Graph
nest 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
nestedCommentAgda.Syntax.Parser.Comments
NeutralLevelAgda.TypeChecking.Level
newArgsMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newArgsMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newCallAgda.Utils.Trace
newCTreeAgda.Auto.NarrowingSearch
newEdgeAgda.Utils.Warshall
NewFlexAgda.Utils.Warshall
newLayoutContextAgda.Syntax.Parser.Layout
newMeta 
1 (Function)Agda.Auto.NarrowingSearch
2 (Function)Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
newMeta'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
NewModuleNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
NewModuleQName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
NewNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
newPlaceholderAgda.Auto.NarrowingSearch
newQuestionMarkAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newRecordMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newRecordMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSortMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSortMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSubConstraintsAgda.Auto.NarrowingSearch
newTelMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newTypeMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newTypeMeta_Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMeta'Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaCtx'Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
nextCharAgda.Syntax.Parser.LookAhead
nextFreshAgda.Utils.Fresh
nextNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nextNodeAgda.Utils.Warshall
nextPolarityAgda.TypeChecking.Conversion
nextSuffixAgda.Utils.Suffix
NiceAgda.Syntax.Concrete.Definitions
NiceConstructorAgda.Syntax.Concrete.Definitions
NiceDeclarationAgda.Syntax.Concrete.Definitions
niceDeclarationsAgda.Syntax.Concrete.Definitions
NiceDefAgda.Syntax.Concrete.Definitions
NiceDefinitionAgda.Syntax.Concrete.Definitions
NiceFieldAgda.Syntax.Concrete.Definitions
NiceImportAgda.Syntax.Concrete.Definitions
NiceModuleAgda.Syntax.Concrete.Definitions
NiceModuleMacroAgda.Syntax.Concrete.Definitions
NiceOpenAgda.Syntax.Concrete.Definitions
NicePragmaAgda.Syntax.Concrete.Definitions
NiceTypeSignatureAgda.Syntax.Concrete.Definitions
No 
1 (Data Constructor)Agda.TypeChecking.Coverage.Match
2 (Data Constructor)Agda.TypeChecking.Patterns.Match
NoAppAgda.TypeChecking.EtaContract
NoBindAgda.Syntax.Internal
NoBindingForBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoBodyAgda.Syntax.Internal
noConstraintsAgda.TypeChecking.Constraints
Node 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Positivity
NodeIdAgda.Utils.Warshall
nodeMapAgda.Utils.Warshall
nodesAgda.Utils.Graph
NoExpectedFailureAgda.Utils.QuickCheck
NoFunVAgda.Syntax.Internal
NoIdAgda.Auto.Syntax
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep'Agda.Auto.Typecheck
NoLayoutAgda.Syntax.Parser.Monad
noLiteralsAgda.TypeChecking.Test.Generators
noMatchLitAgda.TypeChecking.Coverage.Match
noModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
noMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
NoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName_Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NonApplicationAgda.Syntax.Abstract.Views
NonAssocAgda.Syntax.Fixity
NonEmptyAgda.Utils.QuickCheck
NonEmptyListAgda.Utils.QuickCheck
nonfixPAgda.Syntax.Concrete.Operators.Parser
NonNegative 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
NonPositivelyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonZero 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
NoParentAgda.Utils.Trace
NoParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoParseForLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noPatternMatchingOnCodataAgda.TypeChecking.Rules.LHS
NopeAgda.Syntax.Info
NoPrioAgda.Auto.NarrowingSearch
noPropAgda.TypeChecking.Test.Generators
noRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
NoReductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoRHSRequiresAbsurdPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
norm 
1 (Function)Agda.Auto.Typecheck
2 (Function)Agda.Auto.Convert
normalAgda.Syntax.Parser.Lexer
NormaliseAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
normaliseAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
NormalisedAgda.Interaction.BasicOps
normalMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noShadowingOfConstructorsAgda.TypeChecking.Rules.LHS
noShrinkAgda.TypeChecking.Test.Generators
NoSuchBuiltinNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchNameAgda.TypeChecking.Implicit
NoSuchPrimitiveFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuffixAgda.Utils.Suffix
not'Agda.Syntax.Parser.Alex
NotADatatypeAgda.TypeChecking.Coverage
notAHaskellKindAgda.Compiler.HaskellTypes
notAHaskellTypeAgda.Compiler.HaskellTypes
NotAllowedInMutualAgda.Syntax.Concrete.Definitions
NotAModuleExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAnExpressionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAProperTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAValidLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotBAgda.Auto.NarrowingSearch
NotBlockedAgda.Syntax.Internal
notBlockedAgda.Syntax.Internal
NotDelayedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noteAgda.Interaction.Highlighting.Precise
NotFoundAgda.Interaction.FindFile
NotHidden 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Common
notHiddenFreqAgda.TypeChecking.Test.Generators
NothingAgda.Utils.Maybe
NothingAppliedToHiddenArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingToSplitAgda.TypeChecking.Rules.LHS.Problem
nothingToSplitErrorAgda.TypeChecking.Rules.LHS.Instantiate
NotImplementedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInductiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInjectiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notInScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
NotLeqSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotMAgda.Auto.NarrowingSearch
NotPBAgda.Auto.NarrowingSearch
noTraceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notSoNiceDeclarationsAgda.Syntax.Concrete.Definitions
NotStrictlyPositiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotSupportedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoType 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
NoUnifyAgda.TypeChecking.Rules.LHS.Unify
NoWhereAgda.Syntax.Concrete
NoWithFunctionAgda.TypeChecking.Rules.Def
nPiAgda.TypeChecking.Primitive
nsModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nsNamesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NumberAgda.Interaction.Highlighting.Precise
numOfMainSAgda.Compiler.Alonzo.Main
numOfNameAgda.Compiler.Alonzo.Names
numOfQNameAgda.Compiler.Alonzo.Names
numTestsAgda.Utils.QuickCheck