[Agda] overlapping patters

Sergei Meshveliani mechvel at botik.ru
Tue Mar 12 19:00:03 CET 2019


Dear Agda developers,

I have a function defined by several patterns, and it is type-checked.
But the first pattern is a special case of the second one. And after its
removal the program remains type-checked. 

Is Agda (Development, January 1, 2019) supposed to report about such
overlaps?  

Thanks,

------
Sergei



More information about the Agda mailing list