Classes for Zero and One

ink

class Zero (α : Type u) : Type u

• zero : α

ink

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

Equations

• Zero.toOfNat0 = { ofNat := Zero.zero }

ink

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

Equations

• Zero.ofOfNat0 = { zero := 0 }

ink

class One (α : Type u) : Type u

• one : α

ink

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

Equations

• One.toOfNat1 = { ofNat := One.one }

ink

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

Equations

• One.ofOfNat1 = { one := 1 }

ink

@[match_pattern]

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

Equations

• bit0 a = a + a

ink

@[match_pattern]

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

Equations

• bit1 a = bit0 a + 1