fin pattern matching less smart?

Stream: lean4

[Michael Jam]

On nightly-2021-08-21 (commit 9686910c72aa) lean4 was somehow smart enough to realize other cases are not needed:

open Fin in
example : Fin 2 → Nat
| mk 0 _ => 0
| mk 1 _ => 0

From nightly-2021-08-22 (commit 38ecb25d2815) to today nightly-2021-08-23 (commit 4dccaa963b0d), it says:
error: missing cases: (mk (Nat.succ (Nat.succ _)) _)
It's a minor issue as one can add a line to handle the impossible case. I just wanted to notify it in case it was not intended.

[Leonardo de Moura]

See https://github.com/leanprover/lean4/issues/644