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, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
namedMetaOf | Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop |
NamedName | Agda.Syntax.Common |
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 |
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 |
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 |
natSize | Agda.Utils.Size |
NeedOptionCopatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NeedOptionProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NeedOptionRewriting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NeedOptionTwoLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NegApp | Agda.Utils.Haskell.Syntax |
Negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
negative | Agda.TypeChecking.SizedTypes.WarshallSolver |
NegativeUnification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
negPlusKView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
neighbours | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
neighboursMap | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
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 |
NewFlex | Agda.Utils.Warshall |
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 |
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 |
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 |
newPtr | Agda.Utils.Pointer |
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 |
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 |
nextNode | Agda.Utils.Warshall |
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 |
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, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
nmSuggestion | 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 |
NoApp | Agda.TypeChecking.EtaContract |
NoArg | Agda.Interaction.Options |
noAug | Agda.Termination.CallMatrix |
NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NoBindingForPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.Utils.Warshall |
3 (Type/Class) | Agda.TypeChecking.Serialise.Base |
4 (Type/Class) | Agda.TypeChecking.Positivity |
5 (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 |
NodeId | Agda.Utils.Warshall |
NodeInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
NodeK | Agda.Syntax.Concrete.Operators.Parser.Monad |
nodeMap | Agda.Utils.Warshall |
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 |
NoEllipsis | Agda.Syntax.Common |
NoErasedMatches | 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 |
NoGuardednessFlag | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NoGuardednessFlag_ | Agda.Interaction.Options.Warnings |
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
nonConstraining | Agda.TypeChecking.Constraints |
None | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NonEmpty | Agda.Utils.List1 |
nonEmpty | Agda.Utils.List1 |
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 |
NonfixK | Agda.Syntax.Concrete.Operators.Parser.Monad |
NonfixNotation | Agda.Syntax.Notation |
nonIncreasing | Agda.Termination.Order |
NonInteractive | 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 |
NonStrict | Agda.Syntax.Common |
nonStrictToIrr | Agda.Syntax.Common |
nonStrictToRel | Agda.Syntax.Common |
NonTerminating | Agda.Syntax.Common |
NonTerminatingReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Nonvariant | 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 |
NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NoPlaceholder | Agda.Syntax.Common |
noPlaceholder | Agda.Syntax.Common |
NoPositivityCheck | Agda.Syntax.Common |
NoPositivityCheckPragma | Agda.Syntax.Concrete |
NoPostfix | Agda.TypeChecking.ProjectionLike |
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 |
NoRHSRequiresAbsurdPattern | 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 |
NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NoSuchName | Agda.TypeChecking.Implicit |
NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
NotAffectedByOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NotAffectedByOpaque_ | Agda.Interaction.Options.Warnings |
notaFixity | Agda.Syntax.Notation |
notaIsOperator | Agda.Syntax.Notation |
noTakenNames | Agda.Syntax.Translation.AbstractToConcrete |
NotAllowedInMutual | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
NotAllowedInMutual_ | Agda.Interaction.Options.Warnings |
NotAModuleExpr | 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 |
NotAProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 | 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 |
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 |
NothingAppliedToHiddenArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NothingAppliedToInstanceArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NothingToPrune | Agda.TypeChecking.MetaVars.Occurs |
NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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_ | Agda.Interaction.Options.Warnings |
NotInstanceDef | Agda.Syntax.Common |
NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NotMacroDef | Agda.Syntax.Common |
NotMain | Agda.Syntax.Common, Agda.Compiler.Common, Agda.Compiler.Backend |
notMasked | Agda.Termination.Monad |
notMember | |
1 (Function) | Agda.Utils.BoolSet |
2 (Function) | Agda.Utils.Bag |
3 (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 |
notUnderOpaque | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
NotValidBeforeField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 (Type/Class) | Agda.Utils.Null |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
3 (Data Constructor) | Agda.Interaction.JSON |
null | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.BoolSet |
3 (Function) | Agda.Utils.Bag |
4 (Function) | Agda.Utils.Null |
5 (Function) | Agda.Utils.SmallSet |
Number | |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Interaction.JSON |
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 |