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 |
nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
nameConcrete | Agda.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 |
named | Agda.Syntax.Common |
NamedArg | Agda.Syntax.Common |
NamedClause | |
1 (Type/Class) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
2 (Data Constructor) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
namedThing | Agda.Syntax.Common |
nameFixity | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
nameFreq | Agda.TypeChecking.Test.Generators |
NameFreqs | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
nameFreqs | Agda.TypeChecking.Test.Generators |
NameId | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
nameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
NameKind | Agda.Interaction.Highlighting.Precise |
nameModifiers | Agda.Interaction.GhciTop |
nameOf | Agda.Syntax.Common |
nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
nameOfFlat | Agda.TypeChecking.Rules.Builtin.Coinduction |
nameOfInf | Agda.TypeChecking.Rules.Builtin.Coinduction |
nameOfSharp | Agda.TypeChecking.Rules.Builtin.Coinduction |
NamePart | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
nameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
NamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
namesInScope | Agda.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 |
nameSpaceAccess | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
NameSpaceId | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
nameStringParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
nameSupply | Agda.Compiler.Epic.CompileState |
NameTag | Agda.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 |
natPrimTF | Agda.Compiler.Epic.Primitive |
natural | Agda.Utils.TestHelpers |
neg | Agda.TypeChecking.Polarity |
Negative | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
negtype | Agda.Auto.Convert |
neighbours | Agda.Utils.Graph |
nest | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
nestedComment | Agda.Syntax.Parser.Comments |
NeutralLevel | Agda.Syntax.Internal |
newArgsMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newArgsMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newCTree | Agda.Auto.NarrowingSearch |
newEdge | Agda.Utils.Warshall |
NewFlex | Agda.Utils.Warshall |
newIFSMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newIFSMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newLayoutContext | Agda.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 |
NewModuleName | Agda.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 |
NewName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
newName | Agda.Compiler.Epic.CompileState |
NewNotation | Agda.Syntax.Fixity |
newOKHandle | Agda.Auto.NarrowingSearch |
newPlaceholder | Agda.Auto.NarrowingSearch |
newProblem | Agda.TypeChecking.Constraints |
newProblem_ | Agda.TypeChecking.Constraints |
newQuestionMark | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newRecordMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newRecordMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newSortMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newSortMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newSubConstraints | Agda.Auto.NarrowingSearch |
newTelMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newTypeMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newTypeMeta_ | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newValueMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newValueMeta' | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newValueMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
newValueMetaCtx' | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
nextChar | Agda.Syntax.Parser.LookAhead |
nextFresh | Agda.Utils.Fresh |
nextName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
nextNode | Agda.Utils.Warshall |
nextPolarity | Agda.TypeChecking.Conversion |
nextSplit | Agda.TypeChecking.CompiledClause.Compile |
nextSuffix | Agda.Utils.Suffix |
Nice | Agda.Syntax.Concrete.Definitions |
NiceConstructor | Agda.Syntax.Concrete.Definitions |
NiceDataSig | Agda.Syntax.Concrete.Definitions |
NiceDeclaration | Agda.Syntax.Concrete.Definitions |
niceDeclarations | Agda.Syntax.Concrete.Definitions |
NiceField | 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 |
NicePragma | Agda.Syntax.Concrete.Definitions |
NiceRecSig | Agda.Syntax.Concrete.Definitions |
NiceTypeSignature | Agda.Syntax.Concrete.Definitions |
No | |
1 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
2 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
NoAbs | Agda.Syntax.Internal |
NoApp | Agda.TypeChecking.EtaContract |
NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noblks | Agda.Auto.Typecheck |
NoBody | Agda.Syntax.Internal |
noCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noConstraints | Agda.TypeChecking.Constraints |
Node | |
1 (Type/Class) | Agda.Utils.Warshall |
2 (Type/Class) | Agda.TypeChecking.Positivity |
NodeId | Agda.Utils.Warshall |
nodeMap | Agda.Utils.Warshall |
nodes | Agda.Utils.Graph |
NoElim | Agda.TypeChecking.Eliminators |
NoExpectedFailure | Agda.Utils.QuickCheck |
noFixity | Agda.Syntax.Fixity |
NoId | Agda.Auto.Syntax |
NoInsertNeeded | Agda.TypeChecking.Implicit |
NoInv | Agda.TypeChecking.Injectivity |
noiotastep | Agda.Auto.Typecheck |
noiotastep_term | Agda.Auto.Typecheck |
NoLayout | Agda.Syntax.Parser.Monad |
noLiterals | Agda.TypeChecking.Test.Generators |
noMatchLit | Agda.TypeChecking.Coverage.Match |
noModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
noMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
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 |
NonEmpty | Agda.Utils.QuickCheck |
NonEmptyList | Agda.Utils.QuickCheck |
nonfixP | Agda.Syntax.Concrete.Operators.Parser |
NonNegative | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
noNotation | Agda.Syntax.Notation |
NonPositively | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NonStrict | Agda.Syntax.Common |
nonStrictToIrr | Agda.TypeChecking.Irrelevance |
NonZero | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
NoOccurrence | Agda.TypeChecking.Free |
NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noPatternMatchingOnCodata | Agda.TypeChecking.Rules.LHS |
Nope | Agda.Syntax.Info |
noPostponing | Agda.TypeChecking.Rules.LHS.Unify |
NoPrio | Agda.Auto.NarrowingSearch |
noProp | Agda.TypeChecking.Test.Generators |
noRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
NoRecordConstructor | Agda.TypeChecking.Coverage |
NoReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoRHSRequiresAbsurdPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
norm | Agda.Auto.Convert |
normal | Agda.Syntax.Parser.Lexer |
NormalHole | Agda.Syntax.Notation |
Normalise | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
normalise | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
Normalised | Agda.Interaction.BasicOps |
normaliseStatic | Agda.Compiler.Epic.Static |
normalMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noShadowingOfConstructors | Agda.TypeChecking.Rules.LHS |
noShrink | Agda.TypeChecking.Test.Generators |
NoSuchBuiltinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoSuchName | Agda.TypeChecking.Implicit |
NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoSuffix | Agda.Utils.Suffix |
not' | Agda.Syntax.Parser.Alex |
NotADatatype | Agda.TypeChecking.Coverage |
notAHaskellKind | Agda.Compiler.HaskellTypes |
notAHaskellType | Agda.Compiler.HaskellTypes |
noTakenNames | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
NotAllowedInMutual | Agda.Syntax.Concrete.Definitions |
NotAModuleExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotAnExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Notation | Agda.Syntax.Notation |
NotAValidLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotB | Agda.Auto.NarrowingSearch |
NotBlocked | Agda.Syntax.Internal |
notBlocked | Agda.Syntax.Internal |
NotDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
note | Agda.Interaction.Highlighting.Precise |
notequal | Agda.Auto.CaseSplit |
NotForced | Agda.Compiler.Epic.Interface |
notForced | Agda.Compiler.Epic.Interface |
NotFound | Agda.Interaction.FindFile |
NotHidden | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Common |
notHiddenFreq | Agda.TypeChecking.Test.Generators |
Nothing | Agda.Utils.Maybe |
NothingAppliedToHiddenArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NothingAppliedToInstanceArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NothingToPrune | Agda.TypeChecking.MetaVars.Occurs |
NothingToSplit | Agda.TypeChecking.Rules.LHS.Problem |
nothingToSplitError | Agda.TypeChecking.Rules.LHS.Instantiate |
NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotInductive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notInScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotM | Agda.Auto.NarrowingSearch |
NotPB | Agda.Auto.NarrowingSearch |
NotReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notSoNiceDeclarations | Agda.Syntax.Concrete.Definitions |
NotStrictlyPositive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoType | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
NoUnfold | Agda.TypeChecking.MetaVars.Occurs |
NoUnify | Agda.TypeChecking.Rules.LHS.Unify |
NoWhere | Agda.Syntax.Concrete |
NoWithFunction | Agda.TypeChecking.Rules.Def |
nowSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
nPi | Agda.TypeChecking.Primitive |
nrBinds | Agda.Compiler.Epic.Injection |
nrRel | Agda.Compiler.Epic.NatDetection |
nsModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
nsNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
Number | Agda.Interaction.Highlighting.Precise |
numPars | Agda.Compiler.JS.Compiler |
numShrinks | Agda.Utils.QuickCheck |
numTests | Agda.Utils.QuickCheck |
numVars | Agda.Compiler.JS.Case |
numVars' | Agda.Compiler.JS.Case |