Documentation

Init.GrindInstances.ToInt

Instances for concrete types #

instance Lean.Grind.instToIntIntIi :

ToInt Int IntInterval.ii

Equations

Lean.Grind.instToIntIntIi = { toInt := id, toInt_inj := Lean.Grind.instToIntIntIi._proof_1, toInt_mem := Lean.Grind.instToIntIntIi._proof_2 }

@[simp]

theorem Lean.Grind.toInt_int (x : Int) :

↑x = x

instance Lean.Grind.instZeroIntIi :

ToInt.Zero Int IntInterval.ii

instance Lean.Grind.instOfNatIntIi :

ToInt.OfNat Int IntInterval.ii

instance Lean.Grind.instAddIntIi :

ToInt.Add Int IntInterval.ii

instance Lean.Grind.instNegIntIi :

ToInt.Neg Int IntInterval.ii

instance Lean.Grind.instSubIntIi :

ToInt.Sub Int IntInterval.ii

instance Lean.Grind.instMulIntIi :

ToInt.Mul Int IntInterval.ii

instance Lean.Grind.instPowIntIi :

ToInt.Pow Int IntInterval.ii

instance Lean.Grind.instModIntIi :

ToInt.Mod Int IntInterval.ii

instance Lean.Grind.instDivIntIi :

ToInt.Div Int IntInterval.ii

instance Lean.Grind.instLEIntIi :

ToInt.LE Int IntInterval.ii

instance Lean.Grind.instLTIntIi :

ToInt.LT Int IntInterval.ii

instance Lean.Grind.instToIntNatCiOfNatInt :

ToInt Nat (IntInterval.ci 0)

Equations

Lean.Grind.instToIntNatCiOfNatInt = { toInt := Nat.cast, toInt_inj := Lean.Grind.instToIntNatCiOfNatInt._proof_2, toInt_mem := Lean.Grind.instToIntNatCiOfNatInt._proof_1 }

@[simp]

theorem Lean.Grind.toInt_nat (x : Nat) :

↑x = ↑x

instance Lean.Grind.instZeroNatCiOfNatInt :

ToInt.Zero Nat (IntInterval.ci 0)

instance Lean.Grind.instOfNatNatCiOfNatInt :

ToInt.OfNat Nat (IntInterval.ci 0)

instance Lean.Grind.instAddNatCiOfNatInt :

ToInt.Add Nat (IntInterval.ci 0)

instance Lean.Grind.instMulNatCiOfNatInt :

ToInt.Mul Nat (IntInterval.ci 0)

instance Lean.Grind.instPowNatCiOfNatInt :

ToInt.Pow Nat (IntInterval.ci 0)

instance Lean.Grind.instSubNatCiOfNatInt :

ToInt.Sub Nat (IntInterval.ci 0)

instance Lean.Grind.instModNatCiOfNatInt :

ToInt.Mod Nat (IntInterval.ci 0)

instance Lean.Grind.instDivNatCiOfNatInt :

ToInt.Div Nat (IntInterval.ci 0)

instance Lean.Grind.instLENatCiOfNatInt :

ToInt.LE Nat (IntInterval.ci 0)

instance Lean.Grind.instLTNatCiOfNatInt :

ToInt.LT Nat (IntInterval.ci 0)

instance Lean.Grind.instToIntFinCoOfNatIntCast {n : Nat} :

ToInt (Fin n) (IntInterval.co 0 ↑n)

Equations

Lean.Grind.instToIntFinCoOfNatIntCast = { toInt := fun (x : Fin n) => ↑↑x, toInt_inj := ⋯, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_fin {n : Nat} (x : Fin n) :

↑x = ↑↑x

instance Lean.Grind.instZeroFinCoOfNatIntCast {n : Nat} [NeZero n] :

ToInt.Zero (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instOfNatFinCoOfNatIntCast {n : Nat} [NeZero n] :

ToInt.OfNat (Fin n) (IntInterval.co 0 ↑n)

theorem Lean.Grind.ofNat_FinZero (n : Nat) [NeZero n] :

↑(OfNat.ofNat 0) = 0

instance Lean.Grind.instAddFinCoOfNatIntCast {n : Nat} :

ToInt.Add (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instMulFinCoOfNatIntCast {n : Nat} :

ToInt.Mul (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instModFinCoOfNatIntCast {n : Nat} :

ToInt.Mod (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instDivFinCoOfNatIntCast {n : Nat} :

ToInt.Div (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instLEFinCoOfNatIntCast {n : Nat} :

ToInt.LE (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instLTFinCoOfNatIntCast {n : Nat} :

ToInt.LT (Fin n) (IntInterval.co 0 ↑n)

instance Lean.Grind.instToIntUInt8UintOfNatNat :

ToInt UInt8 (IntInterval.uint 8)

Equations

Lean.Grind.instToIntUInt8UintOfNatNat = { toInt := fun (x : UInt8) => ↑x.toNat, toInt_inj := Lean.Grind.instToIntUInt8UintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_uint8 (x : UInt8) :

↑x = ↑x.toNat

instance Lean.Grind.instZeroUInt8UintOfNatNat :

ToInt.Zero UInt8 (IntInterval.uint 8)

instance Lean.Grind.instOfNatUInt8UintOfNatNat :

ToInt.OfNat UInt8 (IntInterval.uint 8)

instance Lean.Grind.instAddUInt8UintOfNatNat :

ToInt.Add UInt8 (IntInterval.uint 8)

instance Lean.Grind.instMulUInt8UintOfNatNat :

ToInt.Mul UInt8 (IntInterval.uint 8)

instance Lean.Grind.instModUInt8UintOfNatNat :

ToInt.Mod UInt8 (IntInterval.uint 8)

instance Lean.Grind.instDivUInt8UintOfNatNat :

ToInt.Div UInt8 (IntInterval.uint 8)

instance Lean.Grind.instLEUInt8UintOfNatNat :

ToInt.LE UInt8 (IntInterval.uint 8)

instance Lean.Grind.instLTUInt8UintOfNatNat :

ToInt.LT UInt8 (IntInterval.uint 8)

instance Lean.Grind.instToIntUInt16UintOfNatNat :

ToInt UInt16 (IntInterval.uint 16)

Equations

Lean.Grind.instToIntUInt16UintOfNatNat = { toInt := fun (x : UInt16) => ↑x.toNat, toInt_inj := Lean.Grind.instToIntUInt16UintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_uint16 (x : UInt16) :

↑x = ↑x.toNat

instance Lean.Grind.instZeroUInt16UintOfNatNat :

ToInt.Zero UInt16 (IntInterval.uint 16)

instance Lean.Grind.instOfNatUInt16UintOfNatNat :

ToInt.OfNat UInt16 (IntInterval.uint 16)

instance Lean.Grind.instAddUInt16UintOfNatNat :

ToInt.Add UInt16 (IntInterval.uint 16)

instance Lean.Grind.instMulUInt16UintOfNatNat :

ToInt.Mul UInt16 (IntInterval.uint 16)

instance Lean.Grind.instModUInt16UintOfNatNat :

ToInt.Mod UInt16 (IntInterval.uint 16)

instance Lean.Grind.instDivUInt16UintOfNatNat :

ToInt.Div UInt16 (IntInterval.uint 16)

instance Lean.Grind.instLEUInt16UintOfNatNat :

ToInt.LE UInt16 (IntInterval.uint 16)

instance Lean.Grind.instLTUInt16UintOfNatNat :

ToInt.LT UInt16 (IntInterval.uint 16)

instance Lean.Grind.instToIntUInt32UintOfNatNat :

ToInt UInt32 (IntInterval.uint 32)

Equations

Lean.Grind.instToIntUInt32UintOfNatNat = { toInt := fun (x : UInt32) => ↑x.toNat, toInt_inj := Lean.Grind.instToIntUInt32UintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_uint32 (x : UInt32) :

↑x = ↑x.toNat

instance Lean.Grind.instZeroUInt32UintOfNatNat :

ToInt.Zero UInt32 (IntInterval.uint 32)

instance Lean.Grind.instOfNatUInt32UintOfNatNat :

ToInt.OfNat UInt32 (IntInterval.uint 32)

instance Lean.Grind.instAddUInt32UintOfNatNat :

ToInt.Add UInt32 (IntInterval.uint 32)

instance Lean.Grind.instMulUInt32UintOfNatNat :

ToInt.Mul UInt32 (IntInterval.uint 32)

instance Lean.Grind.instModUInt32UintOfNatNat :

ToInt.Mod UInt32 (IntInterval.uint 32)

instance Lean.Grind.instDivUInt32UintOfNatNat :

ToInt.Div UInt32 (IntInterval.uint 32)

instance Lean.Grind.instLEUInt32UintOfNatNat :

ToInt.LE UInt32 (IntInterval.uint 32)

instance Lean.Grind.instLTUInt32UintOfNatNat :

ToInt.LT UInt32 (IntInterval.uint 32)

instance Lean.Grind.instToIntUInt64UintOfNatNat :

ToInt UInt64 (IntInterval.uint 64)

Equations

Lean.Grind.instToIntUInt64UintOfNatNat = { toInt := fun (x : UInt64) => ↑x.toNat, toInt_inj := Lean.Grind.instToIntUInt64UintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_uint64 (x : UInt64) :

↑x = ↑x.toNat

instance Lean.Grind.instZeroUInt64UintOfNatNat :

ToInt.Zero UInt64 (IntInterval.uint 64)

instance Lean.Grind.instOfNatUInt64UintOfNatNat :

ToInt.OfNat UInt64 (IntInterval.uint 64)

instance Lean.Grind.instAddUInt64UintOfNatNat :

ToInt.Add UInt64 (IntInterval.uint 64)

instance Lean.Grind.instMulUInt64UintOfNatNat :

ToInt.Mul UInt64 (IntInterval.uint 64)

instance Lean.Grind.instModUInt64UintOfNatNat :

ToInt.Mod UInt64 (IntInterval.uint 64)

instance Lean.Grind.instDivUInt64UintOfNatNat :

ToInt.Div UInt64 (IntInterval.uint 64)

instance Lean.Grind.instLEUInt64UintOfNatNat :

ToInt.LE UInt64 (IntInterval.uint 64)

instance Lean.Grind.instLTUInt64UintOfNatNat :

ToInt.LT UInt64 (IntInterval.uint 64)

instance Lean.Grind.instToIntUSizeUintNumBits :

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

Equations

Lean.Grind.instToIntUSizeUintNumBits = { toInt := fun (x : USize) => ↑x.toNat, toInt_inj := Lean.Grind.instToIntUSizeUintNumBits._proof_1, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_usize (x : USize) :

↑x = ↑x.toNat

instance Lean.Grind.instZeroUSizeUintNumBits :

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

instance Lean.Grind.instOfNatUSizeUintNumBits :

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

instance Lean.Grind.instAddUSizeUintNumBits :

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

instance Lean.Grind.instMulUSizeUintNumBits :

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

instance Lean.Grind.instModUSizeUintNumBits :

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

instance Lean.Grind.instDivUSizeUintNumBits :

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

instance Lean.Grind.instLEUSizeUintNumBits :

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

instance Lean.Grind.instLTUSizeUintNumBits :

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

instance Lean.Grind.instToIntInt8SintOfNatNat :

ToInt Int8 (IntInterval.sint 8)

Equations

Lean.Grind.instToIntInt8SintOfNatNat = { toInt := fun (x : Int8) => x.toInt, toInt_inj := Lean.Grind.instToIntInt8SintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_int8 (x : Int8) :

instance Lean.Grind.instZeroInt8SintOfNatNat :

ToInt.Zero Int8 (IntInterval.sint 8)

instance Lean.Grind.instOfNatInt8SintOfNatNat :

ToInt.OfNat Int8 (IntInterval.sint 8)

instance Lean.Grind.instAddInt8SintOfNatNat :

ToInt.Add Int8 (IntInterval.sint 8)

instance Lean.Grind.instMulInt8SintOfNatNat :

ToInt.Mul Int8 (IntInterval.sint 8)

instance Lean.Grind.instLEInt8SintOfNatNat :

ToInt.LE Int8 (IntInterval.sint 8)

instance Lean.Grind.instLTInt8SintOfNatNat :

ToInt.LT Int8 (IntInterval.sint 8)

instance Lean.Grind.instToIntInt16SintOfNatNat :

ToInt Int16 (IntInterval.sint 16)

Equations

Lean.Grind.instToIntInt16SintOfNatNat = { toInt := fun (x : Int16) => x.toInt, toInt_inj := Lean.Grind.instToIntInt16SintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_int16 (x : Int16) :

instance Lean.Grind.instZeroInt16SintOfNatNat :

ToInt.Zero Int16 (IntInterval.sint 16)

instance Lean.Grind.instOfNatInt16SintOfNatNat :

ToInt.OfNat Int16 (IntInterval.sint 16)

instance Lean.Grind.instAddInt16SintOfNatNat :

ToInt.Add Int16 (IntInterval.sint 16)

instance Lean.Grind.instMulInt16SintOfNatNat :

ToInt.Mul Int16 (IntInterval.sint 16)

instance Lean.Grind.instLEInt16SintOfNatNat :

ToInt.LE Int16 (IntInterval.sint 16)

instance Lean.Grind.instLTInt16SintOfNatNat :

ToInt.LT Int16 (IntInterval.sint 16)

instance Lean.Grind.instToIntInt32SintOfNatNat :

ToInt Int32 (IntInterval.sint 32)

Equations

Lean.Grind.instToIntInt32SintOfNatNat = { toInt := fun (x : Int32) => x.toInt, toInt_inj := Lean.Grind.instToIntInt32SintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_int32 (x : Int32) :

instance Lean.Grind.instZeroInt32SintOfNatNat :

ToInt.Zero Int32 (IntInterval.sint 32)

instance Lean.Grind.instOfNatInt32SintOfNatNat :

ToInt.OfNat Int32 (IntInterval.sint 32)

instance Lean.Grind.instAddInt32SintOfNatNat :

ToInt.Add Int32 (IntInterval.sint 32)

instance Lean.Grind.instMulInt32SintOfNatNat :

ToInt.Mul Int32 (IntInterval.sint 32)

instance Lean.Grind.instLEInt32SintOfNatNat :

ToInt.LE Int32 (IntInterval.sint 32)

instance Lean.Grind.instLTInt32SintOfNatNat :

ToInt.LT Int32 (IntInterval.sint 32)

instance Lean.Grind.instToIntInt64SintOfNatNat :

ToInt Int64 (IntInterval.sint 64)

Equations

Lean.Grind.instToIntInt64SintOfNatNat = { toInt := fun (x : Int64) => x.toInt, toInt_inj := Lean.Grind.instToIntInt64SintOfNatNat._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_int64 (x : Int64) :

instance Lean.Grind.instZeroInt64SintOfNatNat :

ToInt.Zero Int64 (IntInterval.sint 64)

instance Lean.Grind.instOfNatInt64SintOfNatNat :

ToInt.OfNat Int64 (IntInterval.sint 64)

instance Lean.Grind.instAddInt64SintOfNatNat :

ToInt.Add Int64 (IntInterval.sint 64)

instance Lean.Grind.instMulInt64SintOfNatNat :

ToInt.Mul Int64 (IntInterval.sint 64)

instance Lean.Grind.instLEInt64SintOfNatNat :

ToInt.LE Int64 (IntInterval.sint 64)

instance Lean.Grind.instLTInt64SintOfNatNat :

ToInt.LT Int64 (IntInterval.sint 64)

instance Lean.Grind.instToIntBitVecUint {v : Nat} :

ToInt (BitVec v) (IntInterval.uint v)

Equations

Lean.Grind.instToIntBitVecUint = { toInt := fun (x : BitVec v) => ↑x.toNat, toInt_inj := ⋯, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_bitVec {v : Nat} (x : BitVec v) :

↑x = ↑x.toNat

instance Lean.Grind.instZeroBitVecUint {v : Nat} :

ToInt.Zero (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instOfNatBitVecUint {v : Nat} :

ToInt.OfNat (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instAddBitVecUint {v : Nat} :

ToInt.Add (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instMulBitVecUint {v : Nat} :

ToInt.Mul (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instModBitVecUint {v : Nat} :

ToInt.Mod (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instDivBitVecUint {v : Nat} :

ToInt.Div (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instLEBitVecUint {v : Nat} :

ToInt.LE (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instLTBitVecUint {v : Nat} :

ToInt.LT (BitVec v) (IntInterval.uint v)

instance Lean.Grind.instToIntISizeSintNumBits :

ToInt ISize (IntInterval.sint System.Platform.numBits)

Equations

Lean.Grind.instToIntISizeSintNumBits = { toInt := fun (x : ISize) => x.toInt, toInt_inj := Lean.Grind.instToIntISizeSintNumBits._proof_2, toInt_mem := ⋯ }

@[simp]

theorem Lean.Grind.toInt_isize (x : ISize) :

instance Lean.Grind.instZeroISizeSintNumBits :

ToInt.Zero ISize (IntInterval.sint System.Platform.numBits)

instance Lean.Grind.instOfNatISizeSintNumBits :

ToInt.OfNat ISize (IntInterval.sint System.Platform.numBits)

instance Lean.Grind.instAddISizeSintNumBits :

ToInt.Add ISize (IntInterval.sint System.Platform.numBits)

instance Lean.Grind.instMulISizeSintNumBits :

ToInt.Mul ISize (IntInterval.sint System.Platform.numBits)

instance Lean.Grind.instLEISizeSintNumBits :

ToInt.LE ISize (IntInterval.sint System.Platform.numBits)

instance Lean.Grind.instLTISizeSintNumBits :

ToInt.LT ISize (IntInterval.sint System.Platform.numBits)