Stream: new members

Topic: resolve is_some elegantly

Henning Dieterichs (Nov 28 2020 at 14:42):

I have an hypothesis h: ↥(f.is_some). How do I get x: (...) and h: f = some x from it with a single tactic? It works with cases and eliminating the none case, but that is quite involved. I tried rewriting or somehow applying option.get, but that didn't work out. I'm sure that there is a short way!

Shing Tak Lam (Nov 28 2020 at 14:52):

import data.option.basic

example {α : Type} (f : option α) (h : f.is_some) : true :=
begin
set x := option.get h,                      -- x : α
have hx : f = some x := option.get_mem h,   -- hx : f = some x
end


Henning Dieterichs (Nov 28 2020 at 15:24):

thanks, that makes sense! I don't understand the theorem get_mem though... What does \in mean here?

Shing Tak Lam (Nov 28 2020 at 15:26):

example {α : Type}  (a : α) (f : option α) : a ∈ f ↔ f = some a := iff.rfl


so a ∈ f is defined to be f = some a

Henning Dieterichs (Nov 28 2020 at 15:28):

I see. Thanks!

Last updated: May 13 2021 at 06:15 UTC