Commit 2020-04-28 17:54 3c02800d
View on Github →chore(data/dfinsupp): use more precise decidable
requirement (#2535)
Removed decidable_zero_symm
and replaced all [Π i, decidable_pred (eq (0 : β i))]
with [Π i (x : β i), decidable (x ≠ 0)]
. This should work better with open_locale classical
because now the lemmas and definitions don't assume that [Π i (x : β i), decidable (x ≠ 0)]
comes from decidable_zero_symm
.