source
def Lean.Grind.Int8.natCast :
NatCast Int8
Equations

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

Instances For

source
def Lean.Grind.Int8.intCast :
IntCast Int8
Equations

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

Instances For

source
theorem Lean.Grind.Int8.intCast_neg (i : Int) :
↑(-i) = -↑i
source
theorem Lean.Grind.Int8.intCast_ofNat (x : Nat) :
↑(OfNat.ofNat x) = OfNat.ofNat x
source
instance Lean.Grind.instCommRingInt8 :
CommRing Int8
Equations

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

source
instance Lean.Grind.instIsCharPInt8HPowNatOfNat :
IsCharP Int8 (2 ^ 8)
source
instance Lean.Grind.instPowInt8SintOfNatNat :
ToInt.Pow Int8 (IntInterval.sint 8)
source
def Lean.Grind.Int16.natCast :
NatCast Int16
Equations

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

Instances For

source
def Lean.Grind.Int16.intCast :
IntCast Int16
Equations

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

Instances For

source
theorem Lean.Grind.Int16.intCast_neg (i : Int) :
↑(-i) = -↑i
source
theorem Lean.Grind.Int16.intCast_ofNat (x : Nat) :
↑(OfNat.ofNat x) = OfNat.ofNat x
source
instance Lean.Grind.instCommRingInt16 :
CommRing Int16
Equations

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

source
instance Lean.Grind.instIsCharPInt16HPowNatOfNat :
IsCharP Int16 (2 ^ 16)
source
instance Lean.Grind.instPowInt16SintOfNatNat :
ToInt.Pow Int16 (IntInterval.sint 16)
source
def Lean.Grind.Int32.natCast :
NatCast Int32
Equations

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

Instances For

source
def Lean.Grind.Int32.intCast :
IntCast Int32
Equations

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

Instances For

source
theorem Lean.Grind.Int32.intCast_neg (i : Int) :
↑(-i) = -↑i
source
theorem Lean.Grind.Int32.intCast_ofNat (x : Nat) :
↑(OfNat.ofNat x) = OfNat.ofNat x
source
instance Lean.Grind.instCommRingInt32 :
CommRing Int32
Equations

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

source
instance Lean.Grind.instIsCharPInt32HPowNatOfNat :
IsCharP Int32 (2 ^ 32)
source
instance Lean.Grind.instPowInt32SintOfNatNat :
ToInt.Pow Int32 (IntInterval.sint 32)
source
def Lean.Grind.Int64.natCast :
NatCast Int64
Equations

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

Instances For

source
def Lean.Grind.Int64.intCast :
IntCast Int64
Equations

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

Instances For

source
theorem Lean.Grind.Int64.intCast_neg (i : Int) :
↑(-i) = -↑i
source
theorem Lean.Grind.Int64.intCast_ofNat (x : Nat) :
↑(OfNat.ofNat x) = OfNat.ofNat x
source
instance Lean.Grind.instCommRingInt64 :
CommRing Int64
Equations

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

source
instance Lean.Grind.instIsCharPInt64HPowNatOfNat :
IsCharP Int64 (2 ^ 64)
source
instance Lean.Grind.instPowInt64SintOfNatNat :
ToInt.Pow Int64 (IntInterval.sint 64)
source
def Lean.Grind.ISize.natCast :
NatCast ISize
Equations

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

Instances For

source
def Lean.Grind.ISize.intCast :
IntCast ISize
Equations

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

Instances For

source
theorem Lean.Grind.ISize.intCast_neg (i : Int) :
↑(-i) = -↑i
source
theorem Lean.Grind.ISize.intCast_ofNat (x : Nat) :
↑(OfNat.ofNat x) = OfNat.ofNat x
source
instance Lean.Grind.instCommRingISize :
CommRing ISize
Equations

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

source
instance Lean.Grind.instIsCharPISizeHPowNatOfNatNumBits :
IsCharP ISize (2 ^ System.Platform.numBits)
source
instance Lean.Grind.instPowISizeSintNumBits :
ToInt.Pow ISize (IntInterval.sint System.Platform.numBits)