Equations
- (some x).get_or_else _x = x
- none.get_or_else e = e
Equations
- option.get h = x
- option.get h = false.rec α _
@[protected]
Equations
- option.map f o = o.bind (some ∘ f)
@[protected, instance]
Equations
- option.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : option _x), pure x <*> y, map_const := λ (α β : Type u_1), (λ (x : β → α) (y : option β), pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type u_1) (a : option α) (b : option β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : option _x), pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type u_1) (a : option α) (b : option β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : option _x), pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := option.orelse}, failure := none}
@[protected, instance]
Equations
- option.inhabited α = {default := none α}
@[protected, instance]
Equations
- option.decidable_eq (some v₁) (some v₂) = option.decidable_eq._match_1 v₁ v₂ (d v₁ v₂)
- option.decidable_eq (some v₁) none = is_false _
- option.decidable_eq none (some v₂) = is_false _
- option.decidable_eq none none = is_true option.decidable_eq._main._proof_1
- option.decidable_eq._match_1 v₁ v₂ (is_true e) = is_true _
- option.decidable_eq._match_1 v₁ v₂ (is_false n) = is_false _