instance Lean.Grind.instNatCastInt8 : NatCast Int8

Equations

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

instance Lean.Grind.instIntCastInt8 : IntCast Int8

Equations

• Lean.Grind.instIntCastInt8 = { intCast := fun (x : Int) => Int8.ofInt 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)

instance Lean.Grind.instNatCastInt16 : NatCast Int16

Equations

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

instance Lean.Grind.instIntCastInt16 : IntCast Int16

Equations

• Lean.Grind.instIntCastInt16 = { intCast := fun (x : Int) => Int16.ofInt 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)

instance Lean.Grind.instNatCastInt32 : NatCast Int32

Equations

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

instance Lean.Grind.instIntCastInt32 : IntCast Int32

Equations

• Lean.Grind.instIntCastInt32 = { intCast := fun (x : Int) => Int32.ofInt 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)

instance Lean.Grind.instNatCastInt64 : NatCast Int64

Equations

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

instance Lean.Grind.instIntCastInt64 : IntCast Int64

Equations

• Lean.Grind.instIntCastInt64 = { intCast := fun (x : Int) => Int64.ofInt 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)

instance Lean.Grind.instNatCastISize : NatCast ISize

Equations

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

instance Lean.Grind.instIntCastISize : IntCast ISize

Equations

• Lean.Grind.instIntCastISize = { intCast := fun (x : Int) => ISize.ofInt 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)