From 9fc04ae812e2b8d62fae56319968cc8ee0c59ecf Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 22 Jun 2017 18:16:52 -0400 Subject: [PATCH] feat(init/data/option/instances): = none of is_none --- library/init/data/option/instances.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index b6aff8eddf..d256752b4d 100644 --- a/library/init/data/option/instances.lean +++ b/library/init/data/option/instances.lean @@ -43,4 +43,6 @@ lemma option.eq_of_eq_some {α : Type u} : Π {x y : option α}, (∀z, x = some lemma option.eq_some_of_is_some {α : Type u} : Π {o : option α} (h : option.is_some o), o = some (option.get h) | (some x) h := rfl -| none h := false.rec _ $ bool.ff_ne_tt h + +lemma option.eq_none_of_is_none {α : Type u} : Π {o : option α}, o.is_none → o = none +| none h := rfl