Boolean exclusive or
Equations
- Bool.«term_^^_» = Lean.ParserDescr.trailingNode `Bool.«term_^^_» 33 33 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^^ ") (Lean.ParserDescr.cat `term 34))
Instances For
Equations
- x.instDecidableLe y = inferInstanceAs (Decidable (x = true → y = true))
Equations
- x.instDecidableLt y = inferInstanceAs (Decidable ((!x && y) = true))