Zulip Chat Archive

Stream: general

Topic: unoption


Kevin Buzzard (Jul 19 2018 at 18:43):

What is the function which takes a : option X and a proof that a isn't none and returns the x such that a = some x called? I can write it -- but I suspect someone else already thought of it...

Kevin Buzzard (Jul 19 2018 at 18:43):

I found get but that seems to involve bools...

Mario Carneiro (Jul 19 2018 at 18:45):

it is option.get

Mario Carneiro (Jul 19 2018 at 18:45):

you can use a bool as a Prop fyi...

Kevin Buzzard (Jul 19 2018 at 19:48):

OK thanks!


Last updated: Dec 20 2023 at 11:08 UTC