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