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 | 
| YesBelow | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| YesCoverageCheck | 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 |