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