| jComparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| jMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| jMetaType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| join | Agda.Utils.Monad |
| joinHeadMaps | Agda.TypeChecking.Injectivity |
| JointOpacity | Agda.Syntax.Common |
| jointOpacity | Agda.Syntax.Common |
| JSAMD | Agda.Compiler.JS.Pretty |
| jsBackend | Agda.Compiler.JS.Compiler |
| jsBackend' | Agda.Compiler.JS.Compiler |
| JSBackendError | |
| 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 |
| jsBackendErrorName | Agda.TypeChecking.Errors.Names |
| jsBackendErrorNameString | Agda.Interaction.Options.Errors |
| JSBackendError_ | |
| 1 (Type/Class) | Agda.Interaction.Options.Errors |
| 2 (Data Constructor) | Agda.Interaction.Options.Errors |
| jsBackendName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| JSCJS | Agda.Compiler.JS.Pretty |
| jsCoinductionKit | Agda.Compiler.JS.Compiler |
| jsCommandLineFlags | Agda.Compiler.JS.Compiler |
| jsCompile | Agda.Compiler.JS.Compiler |
| jsCompileDef | Agda.Compiler.JS.Compiler |
| JSES6 | Agda.Compiler.JS.Pretty |
| jsFileName | Agda.Compiler.JS.Compiler |
| jsMember | Agda.Compiler.JS.Compiler |
| jsMod | Agda.Compiler.JS.Compiler |
| JSModuleEnv | |
| 1 (Type/Class) | Agda.Compiler.JS.Compiler |
| 2 (Data Constructor) | Agda.Compiler.JS.Compiler |
| JSModuleStyle | Agda.Compiler.JS.Pretty |
| jsonifyHighlightingInfo | Agda.Interaction.Highlighting.JSON |
| JSONKeyOptions | Agda.Interaction.JSON |
| JSONPath | Agda.Interaction.JSON |
| jsonREPL | Agda.Interaction.JSONTop |
| JSOptions | |
| 1 (Type/Class) | Agda.Compiler.JS.Compiler |
| 2 (Data Constructor) | Agda.Compiler.JS.Compiler |
| jsPostCompile | Agda.Compiler.JS.Compiler |
| jsPostModule | Agda.Compiler.JS.Compiler |
| jsPreCompile | Agda.Compiler.JS.Compiler |
| jsPreModule | Agda.Compiler.JS.Compiler |
| JSQName | Agda.Compiler.JS.Syntax |
| Judgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Just | |
| 1 (Data Constructor) | Agda.Utils.Maybe |
| 2 (Data Constructor) | Agda.Utils.Maybe.Strict |
| JustNeg | Agda.TypeChecking.Positivity.Occurrence |
| JustPos | Agda.TypeChecking.Positivity.Occurrence |
| JustRHS | Agda.Syntax.Parser.Helpers |
| JustSort | Agda.Interaction.Base |
| JustType | Agda.Interaction.Base |