Module for exhaustivity checking over pattern matching definitions The algorithm analyses the clauses of a definition one by one from top to bottom, where in each step it has the cases already missing (uncovered), and it generates the new set of missing cases.