theorem UInt8.ofNat_mod_size' {x : Nat} : ofNat (x % 256) = ofNat x

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

instance UInt8.instNatCast : NatCast UInt8

Equations

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

instance UInt8.instIntCast : IntCast UInt8

Equations

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

theorem UInt8.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

theorem UInt16.ofNat_mod_size' {x : Nat} : ofNat (x % 65536) = ofNat x

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

instance UInt16.instNatCast : NatCast UInt16

Equations

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

instance UInt16.instIntCast : IntCast UInt16

Equations

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

theorem UInt16.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

theorem UInt32.ofNat_mod_size' {x : Nat} : ofNat (x % 4294967296) = ofNat x

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

instance UInt32.instNatCast : NatCast UInt32

Equations

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

instance UInt32.instIntCast : IntCast UInt32

Equations

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

theorem UInt32.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

theorem UInt64.ofNat_mod_size' {x : Nat} : ofNat (x % 18446744073709551616) = ofNat x

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

instance UInt64.instNatCast : NatCast UInt64

Equations

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

instance UInt64.instIntCast : IntCast UInt64

Equations

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

theorem UInt64.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance USize.instNatCast : NatCast USize

Equations

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

instance USize.instIntCast : IntCast USize

Equations

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

theorem USize.intCast_ofNat (x : Nat) : ↑(OfNat.ofNat x) = OfNat.ofNat x

instance Lean.Grind.instCommRingUInt8 : CommRing UInt8

Equations

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

instance Lean.Grind.instIsCharPUInt8OfNatNat : IsCharP UInt8 256

instance Lean.Grind.instCommRingUInt16 : CommRing UInt16

Equations

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

instance Lean.Grind.instIsCharPUInt16OfNatNat : IsCharP UInt16 65536

instance Lean.Grind.instCommRingUInt32 : CommRing UInt32

Equations

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

instance Lean.Grind.instIsCharPUInt32OfNatNat : IsCharP UInt32 4294967296

instance Lean.Grind.instCommRingUInt64 : CommRing UInt64

Equations

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

instance Lean.Grind.instIsCharPUInt64OfNatNat : IsCharP UInt64 18446744073709551616

instance Lean.Grind.instCommRingUSize : CommRing USize

Equations

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

instance Lean.Grind.instIsCharPUSizeHPowNatOfNatNumBits : IsCharP USize (2 ^ System.Platform.numBits)