max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(init/data/option/instances): = none of is_none

Browse source
This commit is contained in:
Mario Carneiro 2017-06-22 18:16:52 -04:00 • committed by Leonardo de Moura
parent 0172c17447
commit 9fc04ae812
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/data/option/instances.lean
View file

@ -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