Zulip Chat Archive

Stream: general

Topic: set.sigma_empty

Patrick Massot (Dec 13 2022 at 16:12):

@Yaël Dillies am I right that docs#set.sigma_empty is not what you intended to write?

Patrick Massot (Dec 13 2022 at 16:12):

I'm porting that file to Lean 4 and the simp lemma linter complains about it, and seems right to me.

Patrick Massot (Dec 13 2022 at 16:13):

I guess you intended to write

@[simp] lemma sigma_empty : s.sigma (λ i, (∅ : set (α i))) = ∅ := ext $ λ _, and_false _

Yaël Dillies (Dec 13 2022 at 16:14):

Oh! Yes

Patrick Massot (Dec 13 2022 at 16:16):

It's nice that the Lean 4 linter got better at spotting that simp will never manage to apply this lemma.

Patrick Massot (Dec 13 2022 at 16:16):

If you open a PR to fix this then I'll merge it right away (I mean after CI).

Yaël Dillies (Dec 13 2022 at 16:19):

#17929

Last updated: Dec 20 2023 at 11:08 UTC