instance
Prod.Lex.instDecidableRelProdLex
{α : Type u_1}
{β : Type u_2}
[αeqDec : DecidableEq α]
{r : α → α → Prop}
[rDec : DecidableRel r]
{s : β → β → Prop}
[sDec : DecidableRel s]
:
DecidableRel (Prod.Lex r s)
Equations
- One or more equations did not get rendered due to their size.