IsTrue for Bool -> Prop coercion

Stream: general

[Timo Carlin-Burns]

Mario Carneiro said:

another thing that was floated earlier was to have a IsTrue b function which would be used instead of the current b = true for Bool -> Prop coercion. That would make the expression a bit less "active" since a lot of other stuff keys on equality. For example Chris proposed a simp lemma a = b <-> (a = true <-> b = true) which doesn't really work because it would apply to itself, but it would work if it were spelled using IsTrue

Is there a consensus on this idea? I'm interested in helping move this forward and cleaning up the List API. Is this something that would make sense to experiment with in Mathlib or is the next step here a refactor in std?

[Mario Carneiro]

It requires core changes

[Timo Carlin-Burns]

Ah boolToProp : Coe Bool Prop is from core. So the next step would be an RFC?

[Timo Carlin-Burns]

Ah there is already an RFC and PR from January. lean4#2043 lean4#2060