tsum_bool

Stream: general

[Yaël Dillies]

Why does docs#tsum_bool use decidable.to_bool false/decidable.to_bool true instead of ff/tt?

[Shreyas Srinivas]

Isn't tt and ff a lean 3 thing?

[Ruben Van de Velde]

Yes. docs3#tsum_bool has the same issue, so this is a faithful translation. Still weird, though.

[Reid Barton]

The original Lean 3 source has lemma tsum_bool (f : bool → α) : ∑' i : bool, f i = f false + f true := so it looks like an oversight there.