Finite set literals

Stream: new members

[Martin C. Martin]

Does Lean 3 have a way to write set literals, analogous to {3, 5}?

[Martin C. Martin]

example : {3, 5} = {5, 3} := sorry gives an error.

[Yaël Dillies]

That's because it's ambiguous. Do either

example : ({3, 5} : set ℕ) = {5, 3} := sorry

or

import data.finset.basic

example : ({3, 5} : finset ℕ) = {5, 3} := sorry

depending on which one you mean.

[Martin C. Martin]

Thanks!

[Shreyas Srinivas]

Martin C. Martin said:

Thanks!

I have found it useful to write {5, 3}.toFinset (assuming lean 4)

[Eric Wieser]

I would not recommend using that spelling

[Eric Wieser]

Yaël Dillies' suggestion above is the right spelling

[Shreyas Srinivas]

Okay. I tried this. But when I dealt with definitions or theorems on finsets and I have to use set notation, adding type annotation (on the other side of :=) seemed cumbersome.

[Shreyas Srinivas]

what are the benefits?

[Yaël Dillies]

{5, 3}.toFinset isn't simp normal form.

[Eric Wieser]

The benefits is that the resulting tem is about insert 5 (singleton 3) and not toFinset (insert 5 (singleton 3))