@[instance]
Equations
- prod.inhabited = {default := (inhabited.default α _inst_1, inhabited.default β _inst_2)}
@[instance]
def
prod.decidable_eq
{α : Type u}
{β : Type v}
[h₁ : decidable_eq α]
[h₂ : decidable_eq β] :
decidable_eq (α × β)
Equations
- prod.decidable_eq (a, b) (a', b') = prod.decidable_eq._match_1 a b a' b' (h₁ a a')
- prod.decidable_eq._match_1 a b a' b' (decidable.is_true e₁) = prod.decidable_eq._match_2 a b a' b' e₁ (h₂ b b')
- prod.decidable_eq._match_1 a b a' b' (decidable.is_false n₁) = decidable.is_false _
- prod.decidable_eq._match_2 a b a' b' e₁ (decidable.is_true e₂) = decidable.is_true _
- prod.decidable_eq._match_2 a b a' b' e₁ (decidable.is_false n₂) = decidable.is_false _
@[instance]
def
prod_has_decidable_lt
{α : Type u}
{β : Type v}
[has_lt α]
[has_lt β]
[decidable_eq α]
[decidable_eq β]
[decidable_rel has_lt.lt]
[decidable_rel has_lt.lt]
(s t : α × β) :
Equations
- prod_has_decidable_lt = λ (t s : α × β), or.decidable