def Lean.Grind.Int8.natCast : NatCast Int8

Equations

• Lean.Grind.Int8.natCast = { natCast := fun (x : Nat) => Int8.ofNat x }

def Lean.Grind.Int8.intCast : IntCast Int8

Equations

• Lean.Grind.Int8.intCast = { intCast := fun (x : Int) => Int8.ofInt x }

theorem Lean.Grind.Int8.intCast_neg (i : Int) : ↑(-i) = -↑i

theorem Lean.Grind.Int8.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance Lean.Grind.instCommRingInt8 : CommRing Int8

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Grind.instIsCharPInt8HPowNatOfNat : IsCharP Int8 (2 ^ 8)

instance Lean.Grind.instPowInt8SintOfNatNat : ToInt.Pow Int8 (IntInterval.sint 8)

def Lean.Grind.Int16.natCast : NatCast Int16

Equations

• Lean.Grind.Int16.natCast = { natCast := fun (x : Nat) => Int16.ofNat x }

def Lean.Grind.Int16.intCast : IntCast Int16

Equations

• Lean.Grind.Int16.intCast = { intCast := fun (x : Int) => Int16.ofInt x }

theorem Lean.Grind.Int16.intCast_neg (i : Int) : ↑(-i) = -↑i

theorem Lean.Grind.Int16.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance Lean.Grind.instCommRingInt16 : CommRing Int16

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Grind.instIsCharPInt16HPowNatOfNat : IsCharP Int16 (2 ^ 16)

instance Lean.Grind.instPowInt16SintOfNatNat : ToInt.Pow Int16 (IntInterval.sint 16)

def Lean.Grind.Int32.natCast : NatCast Int32

Equations

• Lean.Grind.Int32.natCast = { natCast := fun (x : Nat) => Int32.ofNat x }

def Lean.Grind.Int32.intCast : IntCast Int32

Equations

• Lean.Grind.Int32.intCast = { intCast := fun (x : Int) => Int32.ofInt x }

theorem Lean.Grind.Int32.intCast_neg (i : Int) : ↑(-i) = -↑i

theorem Lean.Grind.Int32.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance Lean.Grind.instCommRingInt32 : CommRing Int32

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Grind.instIsCharPInt32HPowNatOfNat : IsCharP Int32 (2 ^ 32)

instance Lean.Grind.instPowInt32SintOfNatNat : ToInt.Pow Int32 (IntInterval.sint 32)

def Lean.Grind.Int64.natCast : NatCast Int64

Equations

• Lean.Grind.Int64.natCast = { natCast := fun (x : Nat) => Int64.ofNat x }

def Lean.Grind.Int64.intCast : IntCast Int64

Equations

• Lean.Grind.Int64.intCast = { intCast := fun (x : Int) => Int64.ofInt x }

theorem Lean.Grind.Int64.intCast_neg (i : Int) : ↑(-i) = -↑i

theorem Lean.Grind.Int64.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance Lean.Grind.instCommRingInt64 : CommRing Int64

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Grind.instIsCharPInt64HPowNatOfNat : IsCharP Int64 (2 ^ 64)

instance Lean.Grind.instPowInt64SintOfNatNat : ToInt.Pow Int64 (IntInterval.sint 64)

def Lean.Grind.ISize.natCast : NatCast ISize

Equations

• Lean.Grind.ISize.natCast = { natCast := fun (x : Nat) => ISize.ofNat x }

def Lean.Grind.ISize.intCast : IntCast ISize

Equations

• Lean.Grind.ISize.intCast = { intCast := fun (x : Int) => ISize.ofInt x }

theorem Lean.Grind.ISize.intCast_neg (i : Int) : ↑(-i) = -↑i

theorem Lean.Grind.ISize.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance Lean.Grind.instCommRingISize : CommRing ISize

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Grind.instIsCharPISizeHPowNatOfNatNumBits : IsCharP ISize (2 ^ System.Platform.numBits)

instance Lean.Grind.instPowISizeSintNumBits : ToInt.Pow ISize (IntInterval.sint System.Platform.numBits)