## Stream: general

### Topic: option troubles

#### Johan Commelin (Oct 09 2018 at 18:14):

I have x : option X, and h : x ≠ none. How do I turn this into a y : X such that x = some y? I want to use option.get and option.is_some. But I can't figure out how to use h.

#### Johan Commelin (Oct 09 2018 at 18:15):

example {X : Type} (x : option X) (h : x ≠ none) : X := sorry


#### Johan Commelin (Oct 09 2018 at 18:16):

Or something like that. I should probably not just return an y : X, but also the proof that x = some y.

#### Chris Hughes (Oct 09 2018 at 18:22):

example {α : Sort*} (x : option α) : x ≠ none → {y // x = some y} :=
option.rec_on x (absurd rfl) (λ y _, ⟨y, rfl⟩)


There should be a lemma that says is_some_iff_ne_none, but it seems to be missing.

#### Reid Barton (Oct 09 2018 at 18:23):

Depending on the use, it might be more convenient to just do the cases, absurd at the usage site

#### Johan Commelin (Oct 09 2018 at 18:28):

Thanks @Chris Hughes and @Reid Barton !

#### Patrick Massot (Oct 09 2018 at 18:28):

as in

example {X : Type} (x : option X) (h : x ≠ none) : {y // x = some y} :=
begin
cases x with a,
exact absurd (by simpa [h]) not_false,
exact ⟨a, rfl⟩
end


#### Mario Carneiro (Oct 09 2018 at 18:38):

there is is_none_iff_eq_none, but nothing connecting is_some and is_none. I guess we need a few more variants

#### Mario Carneiro (Oct 09 2018 at 18:38):

but the basic story is option.get is supposed to do this

Last updated: May 08 2021 at 04:14 UTC