Zulip Chat Archive

Stream: lean4

Topic: fin pattern matching less smart?


Michael Jam (Aug 23 2021 at 12:45):

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 (Aug 23 2021 at 12:50):

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


Last updated: Dec 20 2023 at 11:08 UTC