Init.GrindInstances.Ring.UInt

source

theorem UInt8.ofNat_mod_size' {x : Nat} :

ofNat (x % 256) = ofNat x

Variant of UInt8.ofNat_mod_size replacing 2 ^ 8 with 256.

source

def UInt8.natCast :

NatCast UInt8

Equations

UInt8.natCast = { natCast := fun (x : Nat) => UInt8.ofNat x }

Instances For

source

def UInt8.intCast :

IntCast UInt8

Equations

UInt8.intCast = { intCast := fun (x : Int) => UInt8.ofInt x }

Instances For

source

theorem UInt8.intCast_neg (x : Int) :

↑(-x) = -↑x

source

theorem UInt8.intCast_ofNat (x : Nat) :

↑(OfNat.ofNat x) = OfNat.ofNat x

source

theorem UInt16.ofNat_mod_size' {x : Nat} :

ofNat (x % 65536) = ofNat x

Variant of UInt16.ofNat_mod_size replacing 2 ^ 16 with 65536.

source

def UInt16.natCast :

NatCast UInt16

Equations

UInt16.natCast = { natCast := fun (x : Nat) => UInt16.ofNat x }

Instances For

source

def UInt16.intCast :

IntCast UInt16

Equations

UInt16.intCast = { intCast := fun (x : Int) => UInt16.ofInt x }

Instances For

source

theorem UInt16.intCast_neg (x : Int) :

↑(-x) = -↑x

source

theorem UInt16.intCast_ofNat (x : Nat) :

↑(OfNat.ofNat x) = OfNat.ofNat x

source

theorem UInt32.ofNat_mod_size' {x : Nat} :

ofNat (x % 4294967296) = ofNat x

Variant of UInt32.ofNat_mod_size replacing 2 ^ 32 with 4294967296.

source

def UInt32.natCast :

NatCast UInt32

Equations

UInt32.natCast = { natCast := fun (x : Nat) => UInt32.ofNat x }

Instances For

source

def UInt32.intCast :

IntCast UInt32

Equations

UInt32.intCast = { intCast := fun (x : Int) => UInt32.ofInt x }

Instances For

source

theorem UInt32.intCast_neg (x : Int) :

↑(-x) = -↑x

source

theorem UInt32.intCast_ofNat (x : Nat) :

↑(OfNat.ofNat x) = OfNat.ofNat x

source

theorem UInt64.ofNat_mod_size' {x : Nat} :

ofNat (x % 18446744073709551616) = ofNat x

Variant of UInt64.ofNat_mod_size replacing 2 ^ 64 with 18446744073709551616.

source

def UInt64.natCast :

NatCast UInt64

Equations

UInt64.natCast = { natCast := fun (x : Nat) => UInt64.ofNat x }

Instances For

source

def UInt64.intCast :

IntCast UInt64

Equations

UInt64.intCast = { intCast := fun (x : Int) => UInt64.ofInt x }

Instances For

source

theorem UInt64.intCast_neg (x : Int) :

↑(-x) = -↑x

source

theorem UInt64.intCast_ofNat (x : Nat) :

↑(OfNat.ofNat x) = OfNat.ofNat x

source

def USize.natCast :

NatCast USize

Equations

USize.natCast = { natCast := fun (x : Nat) => USize.ofNat x }

Instances For

source

def USize.intCast :

IntCast USize

Equations

USize.intCast = { intCast := fun (x : Int) => USize.ofInt x }

Instances For

source

theorem USize.intCast_neg (x : Int) :

↑(-x) = -↑x

source

theorem USize.intCast_ofNat (x : Nat) :

↑(OfNat.ofNat x) = OfNat.ofNat x

source

instance Lean.Grind.instCommRingUInt8 :

CommRing UInt8

Equations

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

source

instance Lean.Grind.instIsCharPUInt8OfNatNat :

IsCharP UInt8 256

source

instance Lean.Grind.instPowUInt8UintOfNatNat :

ToInt.Pow UInt8 (IntInterval.uint 8)

source

instance Lean.Grind.instCommRingUInt16 :

CommRing UInt16

Equations

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

source

instance Lean.Grind.instIsCharPUInt16OfNatNat :

IsCharP UInt16 65536

source

instance Lean.Grind.instPowUInt16UintOfNatNat :

ToInt.Pow UInt16 (IntInterval.uint 16)

source

instance Lean.Grind.instCommRingUInt32 :

CommRing UInt32

Equations

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

source

instance Lean.Grind.instIsCharPUInt32OfNatNat :

IsCharP UInt32 4294967296

source

instance Lean.Grind.instPowUInt32UintOfNatNat :

ToInt.Pow UInt32 (IntInterval.uint 32)

source

instance Lean.Grind.instCommRingUInt64 :

CommRing UInt64

Equations

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

source

instance Lean.Grind.instIsCharPUInt64OfNatNat :

IsCharP UInt64 18446744073709551616

source

instance Lean.Grind.instPowUInt64UintOfNatNat :

ToInt.Pow UInt64 (IntInterval.uint 64)

source

instance Lean.Grind.instCommRingUSize :

CommRing USize

Equations

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

source

instance Lean.Grind.instIsCharPUSizeHPowNatOfNatNumBits :

IsCharP USize (2 ^ System.Platform.numBits)

source

instance Lean.Grind.instPowUSizeUintNumBits :

ToInt.Pow USize (IntInterval.uint System.Platform.numBits)