List bind provide member of the list proof

Stream: general

[Alice Laroche]

Let's assume foo is a list.
How can i make this work :

do n ← foo
   let h : n ∈ foo := sorry
   baz n foo h

[Adam Topaz]

Can you provide a #mwe ? What happens if foo = []?

[Alice Laroche]

If foo = [] the calculation end here, because the how the list monad work ?

[Yakov Pechersky]

docs#list.attach

[Yakov Pechersky]

do uses a non-dependent bind. We have docs#option.pbind for a dependent bind, but not (yet I guess) for list

[Yakov Pechersky]

So you can do

do n ← foo.attach
   let h : n.val ∈ foo := n.prop
   baz n.val foo h

[Alice Laroche]

Great, thank you