Documentation

Init.GrindInstances.Ring.UInt

theorem UInt8.ofNat_mod_size' {x : Nat} :

ofNat (x % 256) = ofNat x

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

def UInt8.natCast :

Equations

Instances For

def UInt8.intCast :

Equations

Instances For

theorem UInt8.intCast_neg (x : Int) :

↑(-x) = -↑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.

def UInt16.natCast :

Equations

Instances For

def UInt16.intCast :

Equations

Instances For

theorem UInt16.intCast_neg (x : Int) :

↑(-x) = -↑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.

def UInt32.natCast :

Equations

Instances For

def UInt32.intCast :

Equations

Instances For

theorem UInt32.intCast_neg (x : Int) :

↑(-x) = -↑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.

def UInt64.natCast :

Equations

Instances For

def UInt64.intCast :

Equations

Instances For

theorem UInt64.intCast_neg (x : Int) :

↑(-x) = -↑x

theorem UInt64.intCast_ofNat (x : Nat) :

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

def USize.natCast :

Equations

Instances For

def USize.intCast :

Equations

Instances For

theorem USize.intCast_neg (x : Int) :

↑(-x) = -↑x

theorem USize.intCast_ofNat (x : Nat) :

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

instance Lean.Grind.instCommRingUInt8 :

Equations

instance Lean.Grind.instIsCharPUInt8OfNatNat :

IsCharP UInt8 256

instance Lean.Grind.instPowUInt8UintOfNatNat :

ToInt.Pow UInt8 (IntInterval.uint 8)

instance Lean.Grind.instCommRingUInt16 :

CommRing UInt16

Equations

instance Lean.Grind.instIsCharPUInt16OfNatNat :

IsCharP UInt16 65536

instance Lean.Grind.instPowUInt16UintOfNatNat :

ToInt.Pow UInt16 (IntInterval.uint 16)

instance Lean.Grind.instCommRingUInt32 :

CommRing UInt32

Equations

instance Lean.Grind.instIsCharPUInt32OfNatNat :

IsCharP UInt32 4294967296

instance Lean.Grind.instPowUInt32UintOfNatNat :

ToInt.Pow UInt32 (IntInterval.uint 32)

instance Lean.Grind.instCommRingUInt64 :

CommRing UInt64

Equations

instance Lean.Grind.instIsCharPUInt64OfNatNat :

IsCharP UInt64 18446744073709551616

instance Lean.Grind.instPowUInt64UintOfNatNat :

ToInt.Pow UInt64 (IntInterval.uint 64)

instance Lean.Grind.instCommRingUSize :

Equations

instance Lean.Grind.instIsCharPUSizeHPowNatOfNatNumBits :

IsCharP USize (2 ^ System.Platform.numBits)

instance Lean.Grind.instPowUSizeUintNumBits :

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