| jComparison | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| jMetaId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| jMetaType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| joinHeadMaps | Agda.TypeChecking.Injectivity |
| jsBackend | Agda.Compiler.JS.Compiler |
| jsBackend' | Agda.Compiler.JS.Compiler |
| jsBackendName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| jsCoinductionKit | Agda.Compiler.JS.Compiler |
| jsCommandLineFlags | Agda.Compiler.JS.Compiler |
| jsCompile | Agda.Compiler.JS.Compiler |
| jsCompileDef | Agda.Compiler.JS.Compiler |
| 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 |
| json | Agda.Interaction.JSON |
| json' | Agda.Interaction.JSON |
| jsonifyHighlightingInfo | Agda.Interaction.Highlighting.JSON |
| JSONKeyOptions | Agda.Interaction.JSON |
| jsonModeInteractor | Agda.Main |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| Just | |
| 1 (Data Constructor) | Agda.Utils.Maybe |
| 2 (Data Constructor) | Agda.Utils.Maybe.Strict |
| JustNeg | Agda.TypeChecking.Positivity.Occurrence |
| JustPos | Agda.TypeChecking.Positivity.Occurrence |
| JustSort | Agda.Interaction.Base |
| JustType | Agda.Interaction.Base |