Agda-2.3.2.2: test/fail/IncompletePatternMatching.err
IncompletePatternMatching.agda:14,1-15,15 Incomplete pattern matching for _==_. Missing cases: _==_ zero (suc _) _==_ (suc _) zero when checking the definition of _==_
IncompletePatternMatching.agda:14,1-15,15 Incomplete pattern matching for _==_. Missing cases: _==_ zero (suc _) _==_ (suc _) zero when checking the definition of _==_