Problem with looping over finset

Stream: general

[AHan]

Given s : finset ℕ, how can I construct s' : finset (ℕ × ℕ) s.t. ∀ a b, a b ∈ s ↔ (a, b) ∈ s' ?

[Patrick Massot]

I think what you wrote doesn't type-check

[Mario Carneiro]

I assume the a b means a * b

[Patrick Massot]

aren't you busy merging https://github.com/leanprover/mathlib/pull/583?

[Patrick Massot]

Seriously I'd never thought of that interpretation

[AHan]

I mean looping over s, and do something with every two distinct element in s.
(Sorry for my bad English, don't know how to express this well...

[Mario Carneiro]

what are you trying to do in your loop? lean doesn't have "looping constructs" as such

[AHan]

if with list I can do something like

variables {α : Type*}

def test (s : list ℕ) : list ℕ :=
do
    x <- s,
    y <- s,
    [x + y]

[AHan]

I'm just wondering how to do this in if the given type is finset

[Mario Carneiro]

the left arrow is just notation for list.bind, you can call finset.bind and it's just the same

[Mario Carneiro]

I guess there is a missing monad instance for finset that would allow you to use the same notation

[AHan]

Oh! Thanks a lot !!