unoption

Stream: general

[Kevin Buzzard]

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]

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

[Mario Carneiro]

it is option.get

[Mario Carneiro]

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

[Kevin Buzzard]

OK thanks!