You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A while ago, Sebastian suggested[1] that we should redefine the Boolean-to-Prop coercion using a dedicated function. This recently came up again[3] because we're porting material about List.filter, which is now defined on Booleans and thus exercises the coercion heavily.
defBool.asProp (b : Bool) : Prop :=
b = true
instance : Coe Bool Prop where
coe := Bool.asProp
Pros:
No accidental simplification of ¬ b = true to b = false (which requires duplication of simp lemmas).
A while ago, Sebastian suggested[1] that we should redefine the Boolean-to-Prop coercion using a dedicated function. This recently came up again[3] because we're porting material about
List.filter
, which is now defined on Booleans and thus exercises the coercion heavily.Pros:
¬ b = true
tob = false
(which requires duplication of simp lemmas).decide b = b
is defeq (after MakeDecidable
a subtype ofBool
#2038)norm_cast
work out-of-the-box.Cons:
simp only [h]
no longer works as well for a hypothesish : b
withb : Bool
.Original proposal: [1] https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/rfc.3A.20theorem.20names/near/240161960
Other threads:
[2] https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/BEq.20Subtype/near/296650727
[3] https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Prop.20-.3E.20Bool.20regression/near/321996465
The text was updated successfully, but these errors were encountered: