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 |
YesGeneralize | 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 |