Classes for Zero and One

class Zero (α : Type u) : Type u

• zero : α

instance Zero.toOfNat0 {α : Type u_1} [Zero α] : OfNat α 0

instance Zero.ofOfNat0 {α : Type u_1} [OfNat α 0] : Zero α

class One (α : Type u) : Type u

• one : α

instance One.toOfNat1 {α : Type u_1} [One α] : OfNat α 1

instance One.ofOfNat1 {α : Type u_1} [OfNat α 1] : One α

@[match_pattern, deprecated]

def bit0 {α : Type u} [Add α] (a : α) : α

@[match_pattern, deprecated]

def bit1 {α : Type u} [One α] [Add α] (a : α) : α