Index - J
| jMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| jMetaType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| join | Agda.Utils.Monad |
| JS | Agda.Interaction.InteractionTop |
| JSCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| jsFileName | Agda.Compiler.JS.Compiler |
| jsMember | Agda.Compiler.JS.Compiler |
| jsMod | Agda.Compiler.JS.Compiler |
| Judgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| judgToOutputForm | Agda.Interaction.BasicOps |
| Just | |
| 1 (Data Constructor) | Agda.Utils.Maybe |
| 2 (Data Constructor) | Agda.Utils.Maybe.Strict |
| JustNeg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| JustPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| JustSort | Agda.Interaction.BasicOps |
| JustType | Agda.Interaction.BasicOps |