Index - Y
| Yes | |
| 1 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
| YesAbove | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| YesAmbiguous | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| YesBelow | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| YesCatchall | Agda.Syntax.Common |
| YesCoverageCheck | Agda.Syntax.Common |
| YesDisplayLHS | Agda.Syntax.Common |
| YesEta | Agda.Syntax.Common |
| YesGeneralizeMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| YesGeneralizeVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| YesOverlap | Agda.Syntax.Common |
| YesPositivityCheck | Agda.Syntax.Common |
| YesReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| YesSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| yesSimplification | Agda.TypeChecking.Patterns.Match |
| YesUnfold | Agda.TypeChecking.MetaVars.Occurs |
| YesUniverseCheck | Agda.Syntax.Common |