Init.GrindInstances.Ring.SInt

source

@[implicit_reducible]

def Lean.Grind.Int8.natCast :

NatCast Int8

Equations

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

Instances For

source

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

def Lean.Grind.Int16.natCast :

NatCast Int16

Equations

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

Instances For

source

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

def Lean.Grind.Int32.natCast :

NatCast Int32

Equations

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

Instances For

source

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

def Lean.Grind.Int64.natCast :

NatCast Int64

Equations

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

Instances For

source

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

def Lean.Grind.ISize.natCast :

NatCast ISize

Equations

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

Instances For

source

@[implicit_reducible]

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

@[implicit_reducible]

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)