Init.Data.Zero

Module docstring

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

Zero.toOfNat0 instance

{α} [Zero α] : OfNat α (nat_lit 0)

Full source

instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

Zero Element as Numeric Literal Zero

Informal description

For any type $\alpha$ with a zero element (i.e., an instance of `Zero α`), the numeric literal `0` can be interpreted as an element of $\alpha$ (i.e., there exists an instance of `OfNat α 0`).

Zero.ofOfNat0 instance

{α} [OfNat α (nat_lit 0)] : Zero α

Full source

instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

Numeric Literal Zero Implies Zero Structure

Informal description

For any type $\alpha$ with a distinguished element `0` given by the numeric literal interpretation `OfNat α 0`, $\alpha$ is also equipped with a zero element structure `Zero α`.