Zulip Chat Archive

Stream: general

Topic: List bind provide member of the list proof


Alice Laroche (Jan 13 2022 at 19:05):

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 (Jan 13 2022 at 19:09):

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

Alice Laroche (Jan 13 2022 at 19:10):

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

Yakov Pechersky (Jan 13 2022 at 19:13):

docs#list.attach

Yakov Pechersky (Jan 13 2022 at 19:14):

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

Yakov Pechersky (Jan 13 2022 at 19:15):

So you can do

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

Alice Laroche (Jan 13 2022 at 19:16):

Great, thank you


Last updated: Dec 20 2023 at 11:08 UTC