Instances converting between Zero α and OfNat α (nat_lit 0).

@[instance 300]

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

Equations

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

@[instance 200]

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

Equations

• Zero.ofOfNat0 = { zero := 0 }

Instances converting between One α and OfNat α (nat_lit 1).

@[instance 300]

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

Equations

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

@[instance 200]

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

Equations

• One.ofOfNat1 = { one := 1 }