| kanOpBase | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| kanOpCofib | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| KanOperation | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| kanOpName | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| kanOpSides | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| Keep | Agda.Interaction.Base |
| keepComments | Agda.Syntax.Parser.Comments |
| keepCommentsM | Agda.Syntax.Parser.Comments |
| KeepHighlighting | Agda.Interaction.Response |
| KeepMetas | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| KeepNames | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Key | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| 2 (Type/Class) | Agda.Interaction.JSON |
| key | Agda.Utils.Lens |
| keyModifier | Agda.Interaction.JSON |
| keys | |
| 1 (Function) | Agda.Utils.Bag |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Utils.AssocList |
| KeyValue | Agda.Interaction.JSON |
| KeyValueOmit | Agda.Interaction.JSON |
| Keyword | |
| 1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| 2 (Type/Class) | Agda.Syntax.Parser.Tokens |
| keyword | |
| 1 (Function) | Agda.Syntax.Parser.LexActions |
| 2 (Function) | Agda.Interaction.Highlighting.Vim |
| killArgs | Agda.TypeChecking.MetaVars.Occurs |
| killedType | Agda.TypeChecking.MetaVars.Occurs |
| KILLRANGE | Agda.Syntax.Position |
| KillRange | Agda.Syntax.Position |
| killRange | Agda.Syntax.Position |
| killRangeMap | Agda.Syntax.Position |
| killRangeN | Agda.Syntax.Position |
| KillRangeT | Agda.Syntax.Position |
| kind | Agda.Interaction.JSON |
| kind' | Agda.Interaction.JSON |
| kindedThing | Agda.Syntax.Scope.Base |
| KindOfBlock | Agda.Syntax.Concrete.Definitions.Types |
| KindOfForeignCode | Agda.Compiler.MAlonzo.Pragmas |
| KindOfName | Agda.Syntax.Scope.Base |
| kindOfNameToNameKind | Agda.Interaction.Highlighting.Precise |
| KindsOfNames | Agda.Syntax.Scope.Base |
| KName | Agda.Syntax.Abstract.Views |
| KnownBool | Agda.Utils.TypeLits |
| KnownFVs | Agda.Syntax.Common |
| KnownIdent | Agda.Syntax.Concrete |
| KnownOpApp | Agda.Syntax.Concrete |
| KwAbstract | Agda.Syntax.Parser.Tokens |
| KwBUILTIN | Agda.Syntax.Parser.Tokens |
| KwCATCHALL | Agda.Syntax.Parser.Tokens |
| KwCoData | Agda.Syntax.Parser.Tokens |
| KwCoInductive | Agda.Syntax.Parser.Tokens |
| KwCOMPILE | Agda.Syntax.Parser.Tokens |
| KwConstructor | Agda.Syntax.Parser.Tokens |
| KwData | Agda.Syntax.Parser.Tokens |
| KwDISPLAY | Agda.Syntax.Parser.Tokens |
| KwDo | Agda.Syntax.Parser.Tokens |
| KwETA | Agda.Syntax.Parser.Tokens |
| KwEta | Agda.Syntax.Parser.Tokens |
| KwField | Agda.Syntax.Parser.Tokens |
| KwForall | Agda.Syntax.Parser.Tokens |
| KwFOREIGN | Agda.Syntax.Parser.Tokens |
| KwHiding | Agda.Syntax.Parser.Tokens |
| KwImport | Agda.Syntax.Parser.Tokens |
| KwIMPOSSIBLE | Agda.Syntax.Parser.Tokens |
| KwIn | Agda.Syntax.Parser.Tokens |
| KwInductive | Agda.Syntax.Parser.Tokens |
| KwInfix | Agda.Syntax.Parser.Tokens |
| KwInfixL | Agda.Syntax.Parser.Tokens |
| KwInfixR | Agda.Syntax.Parser.Tokens |
| KwINJECTIVE | Agda.Syntax.Parser.Tokens |
| KwINLINE | Agda.Syntax.Parser.Tokens |
| KwInstance | Agda.Syntax.Parser.Tokens |
| KwInterleaved | Agda.Syntax.Parser.Tokens |
| KwLet | Agda.Syntax.Parser.Tokens |
| KwLINE | Agda.Syntax.Parser.Tokens |
| KwMacro | Agda.Syntax.Parser.Tokens |
| KwMEASURE | Agda.Syntax.Parser.Tokens |
| KwModule | Agda.Syntax.Parser.Tokens |
| KwMutual | Agda.Syntax.Parser.Tokens |
| KwNoEta | Agda.Syntax.Parser.Tokens |
| KwNOINLINE | Agda.Syntax.Parser.Tokens |
| KwNON_COVERING | Agda.Syntax.Parser.Tokens |
| KwNON_TERMINATING | Agda.Syntax.Parser.Tokens |
| KwNOT_PROJECTION_LIKE | Agda.Syntax.Parser.Tokens |
| KwNO_POSITIVITY_CHECK | Agda.Syntax.Parser.Tokens |
| KwNO_TERMINATION_CHECK | Agda.Syntax.Parser.Tokens |
| KwNO_UNIVERSE_CHECK | Agda.Syntax.Parser.Tokens |
| KwOpaque | Agda.Syntax.Parser.Tokens |
| KwOpen | Agda.Syntax.Parser.Tokens |
| KwOPTIONS | Agda.Syntax.Parser.Tokens |
| KwOverlap | Agda.Syntax.Parser.Tokens |
| KwPatternSyn | Agda.Syntax.Parser.Tokens |
| KwPOLARITY | Agda.Syntax.Parser.Tokens |
| KwPostulate | Agda.Syntax.Parser.Tokens |
| KwPrimitive | Agda.Syntax.Parser.Tokens |
| KwPrivate | Agda.Syntax.Parser.Tokens |
| KwPublic | Agda.Syntax.Parser.Tokens |
| KwQuote | Agda.Syntax.Parser.Tokens |
| KwQuoteTerm | Agda.Syntax.Parser.Tokens |
| KwRecord | Agda.Syntax.Parser.Tokens |
| KwRenaming | Agda.Syntax.Parser.Tokens |
| KwREWRITE | Agda.Syntax.Parser.Tokens |
| KwRewrite | Agda.Syntax.Parser.Tokens |
| KwSTATIC | Agda.Syntax.Parser.Tokens |
| KwSyntax | Agda.Syntax.Parser.Tokens |
| KwTactic | Agda.Syntax.Parser.Tokens |
| KwTERMINATING | Agda.Syntax.Parser.Tokens |
| KwTo | Agda.Syntax.Parser.Tokens |
| KwUnfolding | Agda.Syntax.Parser.Tokens |
| KwUnquote | Agda.Syntax.Parser.Tokens |
| KwUnquoteDecl | Agda.Syntax.Parser.Tokens |
| KwUnquoteDef | Agda.Syntax.Parser.Tokens |
| KwUsing | Agda.Syntax.Parser.Tokens |
| KwVariable | Agda.Syntax.Parser.Tokens |
| KwWARNING_ON_IMPORT | Agda.Syntax.Parser.Tokens |
| KwWARNING_ON_USAGE | Agda.Syntax.Parser.Tokens |
| KwWhere | Agda.Syntax.Parser.Tokens |
| KwWith | Agda.Syntax.Parser.Tokens |