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.Abstract, Agda.Syntax.Internal |
4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
5 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
nameConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
Named | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
named | Agda.Syntax.Common |
NamedArg | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Type/Class) | Agda.Syntax.Internal |
namedArg | Agda.Syntax.Common |
NamedArgs | Agda.Syntax.Internal |
NamedClause | Agda.Syntax.Translation.InternalToAbstract |
namedClausePats | Agda.Syntax.Internal |
NamedMeta | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
nameFixity | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
NameId | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
nameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
NameKind | Agda.Interaction.Highlighting.Precise |
nameModifiers | Agda.Interaction.InteractionTop |
nameOf | Agda.Syntax.Common |
nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
nameOfFlat | Agda.TypeChecking.Monad.Builtin |
nameOfInf | Agda.TypeChecking.Monad.Builtin |
nameOfSharp | Agda.TypeChecking.Monad.Builtin |
NamePart | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
nameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
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 |
nameStringParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
nameSupply | Agda.Compiler.Epic.CompileState |
NameTag | Agda.Syntax.Scope.Base |
nameToArgName | Agda.Syntax.Internal |
nameToPatVarName | Agda.Syntax.Internal |
nameToRawName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
nameVariant | Agda.Utils.Suffix |
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 |
NeedOptionCopatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
neg | Agda.TypeChecking.Polarity |
Negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
negtype | Agda.Auto.Convert |
neighbours | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | 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 |
newArgsMeta | Agda.TypeChecking.MetaVars |
newArgsMeta' | Agda.TypeChecking.MetaVars |
newArgsMetaCtx | Agda.TypeChecking.MetaVars |
newArgsMetaCtx' | Agda.TypeChecking.MetaVars |
newCTree | Agda.Auto.NarrowingSearch |
newEdge | Agda.Utils.Warshall |
NewFlex | Agda.Utils.Warshall |
newIFSMeta | Agda.TypeChecking.MetaVars |
newIFSMetaCtx | Agda.TypeChecking.MetaVars |
newIORef | Agda.Utils.IORef |
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 |
NewModuleQName | |
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract |
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract |
NewName | Agda.Syntax.Translation.ConcreteToAbstract |
newName | Agda.Compiler.Epic.CompileState |
newNamedValueMeta | Agda.TypeChecking.MetaVars |
NewNotation | |
1 (Type/Class) | Agda.Syntax.Fixity |
2 (Data Constructor) | Agda.Syntax.Fixity |
newOKHandle | Agda.Auto.NarrowingSearch |
newPlaceholder | Agda.Auto.NarrowingSearch |
newProblem | Agda.TypeChecking.Constraints |
newProblem_ | Agda.TypeChecking.Constraints |
newPtr | Agda.Utils.Pointer, Agda.Syntax.Internal |
newQuestionMark | Agda.TypeChecking.MetaVars |
newRecordMeta | Agda.TypeChecking.MetaVars |
newRecordMetaCtx | Agda.TypeChecking.MetaVars |
newSortMeta | Agda.TypeChecking.MetaVars |
newSortMetaCtx | Agda.TypeChecking.MetaVars |
newSubConstraints | Agda.Auto.NarrowingSearch |
newTelMeta | 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 |
nextChar | Agda.Syntax.Parser.LookAhead |
nextFresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
nextName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
nextNode | Agda.Utils.Warshall |
nextPolarity | Agda.TypeChecking.Polarity |
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 |
NiceFunClause | 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 |
NiceRecSig | Agda.Syntax.Concrete.Definitions |
NiceTypeSignature | Agda.Syntax.Concrete.Definitions |
NiceUnquoteDecl | Agda.Syntax.Concrete.Definitions |
nmid | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
nmSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
No | |
1 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
2 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
NoAbs | Agda.Syntax.Internal |
noabsApp | Agda.TypeChecking.Substitute |
NoAmbiguousConstructors | Agda.Syntax.Scope.Base |
NoApp | Agda.TypeChecking.EtaContract |
noAug | Agda.Termination.CallMatrix |
NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noblks | Agda.Auto.Typecheck |
NoBody | Agda.Syntax.Internal |
noColorArg | Agda.Syntax.Common |
noCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noConstraints | Agda.TypeChecking.Constraints |
Node | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
2 (Type/Class) | Agda.Utils.Warshall |
3 (Type/Class) | Agda.Termination.CallGraph |
4 (Type/Class) | Agda.TypeChecking.Positivity |
NodeFlex | Agda.TypeChecking.SizedTypes.WarshallSolver |
nodeFromSizeExpr | Agda.TypeChecking.SizedTypes.WarshallSolver |
NodeId | Agda.Utils.Warshall |
nodeIn | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
NodeInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
nodeMap | Agda.Utils.Warshall |
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 | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
nodeToSizeExpr | Agda.TypeChecking.SizedTypes.WarshallSolver |
NodeZero | Agda.TypeChecking.SizedTypes.WarshallSolver |
NoExpectedFailure | Agda.Utils.QuickCheck |
noFixity | Agda.Syntax.Fixity |
NoFunSig | Agda.Syntax.Abstract |
NoHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
NoLayout | Agda.Syntax.Parser.Monad |
noLiterals | Agda.TypeChecking.Test.Generators |
noMatchLit | Agda.TypeChecking.Coverage.Match |
noModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
noMsg | Agda.Utils.Except |
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 |
None | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NonEmpty | Agda.Utils.QuickCheck |
NonEmptyList | Agda.Utils.QuickCheck |
NonfixNotation | Agda.Syntax.Notation |
nonfixP | Agda.Syntax.Concrete.Operators.Parser |
nonIncreasing | Agda.Termination.Order |
NonInteractive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NonNegative | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
NoNotation | Agda.Syntax.Notation |
noNotation | Agda.Syntax.Notation |
NonPositively | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NonStrict | Agda.Syntax.Common |
nonStrictToIrr | Agda.TypeChecking.Irrelevance |
NonTerminating | Agda.Syntax.Common |
NonTerminatingReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Nonvariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
nonvariantToUnusedArg | Agda.TypeChecking.Polarity |
nonvariantToUnusedArgInClause | Agda.TypeChecking.Polarity |
nonvariantToUnusedArgInDef | Agda.TypeChecking.Polarity |
NonZero | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
NoOccurrence | Agda.TypeChecking.Free |
NoOutputTypeName | Agda.TypeChecking.Telescope |
NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
noPatternMatchingOnCodata | Agda.TypeChecking.Rules.LHS |
noPostponing | Agda.TypeChecking.Rules.LHS.Unify |
NoPrio | Agda.Auto.NarrowingSearch |
noProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest |
NoProjectedVar | Agda.TypeChecking.MetaVars |
noProjectedVar | Agda.TypeChecking.MetaVars |
NoProjection | Agda.TypeChecking.ProjectionLike |
noProp | Agda.TypeChecking.Test.Generators |
noRange | Agda.Syntax.Position |
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 |
normalForm | Agda.Interaction.BasicOps |
NormalHole | Agda.Syntax.Notation |
Normalise | Agda.TypeChecking.Reduce |
normalise | Agda.TypeChecking.Reduce |
normalise' | Agda.TypeChecking.Reduce |
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 |
noShrinking | Agda.Utils.QuickCheck |
NoSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
NotAConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotADatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notaFixity | Agda.Syntax.Fixity |
notAHaskellKind | Agda.Compiler.HaskellTypes |
notAHaskellType | Agda.Compiler.HaskellTypes |
noTakenNames | Agda.Syntax.Translation.AbstractToConcrete |
NotALiteral | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotAllowedInMutual | Agda.Syntax.Concrete.Definitions |
NotAModuleExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notaName | Agda.Syntax.Fixity |
NotAnExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotAProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Notation | Agda.Syntax.Notation |
notation | Agda.Syntax.Fixity |
NotationKind | Agda.Syntax.Notation |
notationKind | Agda.Syntax.Notation |
notationNames | Agda.Syntax.Fixity |
NotAValidLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotB | Agda.Auto.NarrowingSearch |
NotBlocked | Agda.Syntax.Internal |
notBlocked | Agda.Syntax.Internal |
NotComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
NotDelayed | Agda.Syntax.Common |
notDominated | Agda.Utils.Favorites |
note | Agda.Interaction.Highlighting.Precise |
notequal | Agda.Auto.CaseSplit |
NoTerminationCheck | Agda.Syntax.Common |
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 |
notHidden | Agda.Syntax.Common |
notHiddenFreq | Agda.TypeChecking.Test.Generators |
Nothing | |
1 (Data Constructor) | Agda.Utils.Maybe |
2 (Data Constructor) | Agda.Utils.Maybe.Strict |
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.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
NotInstanceDef | Agda.Syntax.Common |
NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotM | Agda.Auto.NarrowingSearch |
NotMainInterface | Agda.Interaction.Imports |
notMember | Agda.Utils.Bag |
NotPB | Agda.Auto.NarrowingSearch |
NotReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notShadowedLocal | Agda.Syntax.Scope.Base |
notShadowedLocals | Agda.Syntax.Scope.Base |
notSoNiceDeclaration | Agda.Syntax.Concrete.Definitions |
NotStrictlyPositive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
NotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
notVisible | Agda.Syntax.Common |
NotWorse | Agda.Termination.Order |
notWorse | Agda.Termination.Order |
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 |
NoWarnings | Agda.Interaction.Imports |
NoWhere | Agda.Syntax.Concrete |
NoWithFunction | Agda.TypeChecking.Rules.Def |
nowReifyingUnquoted | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
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 |
nsNames | Agda.Syntax.Scope.Base |
Null | Agda.Utils.Null |
null | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Utils.Favorites |
4 (Function) | Agda.Utils.Bag |
5 (Function) | Agda.Utils.Null |
6 (Function) | Agda.Termination.CallMatrix |
7 (Function) | Agda.Termination.CallGraph |
Number | Agda.Interaction.Highlighting.Precise |
numberPatVars | Agda.Syntax.Internal.Pattern |
numPars | Agda.Compiler.JS.Compiler |
numShrinkFinal | Agda.Utils.QuickCheck |
numShrinks | Agda.Utils.QuickCheck |
numShrinkTries | Agda.Utils.QuickCheck |
numTests | Agda.Utils.QuickCheck |
numVars | Agda.Compiler.JS.Case |
numVars' | Agda.Compiler.JS.Case |