Pattern matching is limited by overlapping patterns

[refparo]

Consider the following code, which is essentially almost identical to the code in #96, only with the two clauses swapped.

open data Bool : Type 0 | true | false
def not (b : Bool) : Bool
 | false => true
 | otherwise => false

The second clause is intended as a "default" case. Such pattern may be widely used in real-world programming, but Aya (as of 1747794) rejects this. Is this behavior expected? Is it possible to make this type check while also having overlapping patterns?

[ice1000]

It is rejected. The solution would be to let the two styles of function definitions coexist, but we need to work on that. It's not like this is impossible.

[ice1000]

See also #190

[ice1000]

We now support these definitions by default. Overlapping patterns need explicit specification overlap