Agda-2.3.0.1: 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
nameOfFlatAgda.TypeChecking.Rules.Builtin.Coinduction
nameOfInfAgda.TypeChecking.Rules.Builtin.Coinduction
nameOfSharpAgda.TypeChecking.Rules.Builtin.Coinduction
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
nameSpaceAccessAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpaceIdAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nameStringPartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSupplyAgda.Compiler.Epic.CompileState
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
natPrimTFAgda.Compiler.Epic.Primitive
naturalAgda.Utils.TestHelpers
negAgda.TypeChecking.Polarity
NegativeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
negtypeAgda.Auto.Convert
neighboursAgda.Utils.Graph
nest 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
nestedCommentAgda.Syntax.Parser.Comments
NeutralLevelAgda.Syntax.Internal
newArgsMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newArgsMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newCTreeAgda.Auto.NarrowingSearch
newEdgeAgda.Utils.Warshall
NewFlexAgda.Utils.Warshall
newIFSMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newIFSMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
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
newNameAgda.Compiler.Epic.CompileState
NewNotationAgda.Syntax.Fixity
newOKHandleAgda.Auto.NarrowingSearch
newPlaceholderAgda.Auto.NarrowingSearch
newProblemAgda.TypeChecking.Constraints
newProblem_Agda.TypeChecking.Constraints
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
nextSplitAgda.TypeChecking.CompiledClause.Compile
nextSuffixAgda.Utils.Suffix
NiceAgda.Syntax.Concrete.Definitions
NiceConstructorAgda.Syntax.Concrete.Definitions
NiceDataSigAgda.Syntax.Concrete.Definitions
NiceDeclarationAgda.Syntax.Concrete.Definitions
niceDeclarationsAgda.Syntax.Concrete.Definitions
NiceFieldAgda.Syntax.Concrete.Definitions
NiceImportAgda.Syntax.Concrete.Definitions
NiceModuleAgda.Syntax.Concrete.Definitions
NiceModuleMacroAgda.Syntax.Concrete.Definitions
NiceMutualAgda.Syntax.Concrete.Definitions
NiceOpenAgda.Syntax.Concrete.Definitions
NicePragmaAgda.Syntax.Concrete.Definitions
NiceRecSigAgda.Syntax.Concrete.Definitions
NiceTypeSignatureAgda.Syntax.Concrete.Definitions
No 
1 (Data Constructor)Agda.TypeChecking.Coverage.Match
2 (Data Constructor)Agda.TypeChecking.Patterns.Match
NoAbsAgda.Syntax.Internal
NoAppAgda.TypeChecking.EtaContract
NoBindingForBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noblksAgda.Auto.Typecheck
NoBodyAgda.Syntax.Internal
noCompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
NoElimAgda.TypeChecking.Eliminators
NoExpectedFailureAgda.Utils.QuickCheck
noFixityAgda.Syntax.Fixity
NoIdAgda.Auto.Syntax
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep_termAgda.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
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
noNotationAgda.Syntax.Notation
NonPositivelyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonStrictAgda.Syntax.Common
nonStrictToIrrAgda.TypeChecking.Irrelevance
NonZero 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
NoOccurrenceAgda.TypeChecking.Free
NoParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoParseForLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noPatternMatchingOnCodataAgda.TypeChecking.Rules.LHS
NopeAgda.Syntax.Info
noPostponingAgda.TypeChecking.Rules.LHS.Unify
NoPrioAgda.Auto.NarrowingSearch
noPropAgda.TypeChecking.Test.Generators
noRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
NoRecordConstructorAgda.TypeChecking.Coverage
NoReductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoRHSRequiresAbsurdPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
normAgda.Auto.Convert
normalAgda.Syntax.Parser.Lexer
NormalHoleAgda.Syntax.Notation
NormaliseAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
normaliseAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
NormalisedAgda.Interaction.BasicOps
normaliseStaticAgda.Compiler.Epic.Static
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
noTakenNamesAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
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
NotationAgda.Syntax.Notation
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
notequalAgda.Auto.CaseSplit
NotForcedAgda.Compiler.Epic.Interface
notForcedAgda.Compiler.Epic.Interface
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
NothingAppliedToInstanceArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingToPruneAgda.TypeChecking.MetaVars.Occurs
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
NotReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notReducedAgda.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
NoUnfoldAgda.TypeChecking.MetaVars.Occurs
NoUnifyAgda.TypeChecking.Rules.LHS.Unify
NoWhereAgda.Syntax.Concrete
NoWithFunctionAgda.TypeChecking.Rules.Def
nowSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
nPiAgda.TypeChecking.Primitive
nrBindsAgda.Compiler.Epic.Injection
nrRelAgda.Compiler.Epic.NatDetection
nsModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nsNamesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NumberAgda.Interaction.Highlighting.Precise
numParsAgda.Compiler.JS.Compiler
numShrinksAgda.Utils.QuickCheck
numTestsAgda.Utils.QuickCheck
numVarsAgda.Compiler.JS.Case
numVars'Agda.Compiler.JS.Case