## Instances for concrete types #

source
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 }

source
@[simp]
theorem Lean.Grind.toInt_int (x : Int) :
↑x = x
source
instance Lean.Grind.instZeroIntIi :
ToInt.Zero Int IntInterval.ii
source
instance Lean.Grind.instOfNatIntIi :
ToInt.OfNat Int IntInterval.ii
source
instance Lean.Grind.instAddIntIi :
ToInt.Add Int IntInterval.ii
source
instance Lean.Grind.instNegIntIi :
ToInt.Neg Int IntInterval.ii
source
instance Lean.Grind.instSubIntIi :
ToInt.Sub Int IntInterval.ii
source
instance Lean.Grind.instMulIntIi :
ToInt.Mul Int IntInterval.ii
source
instance Lean.Grind.instPowIntIi :
ToInt.Pow Int IntInterval.ii
source
instance Lean.Grind.instModIntIi :
ToInt.Mod Int IntInterval.ii
source
instance Lean.Grind.instDivIntIi :
ToInt.Div Int IntInterval.ii
source
instance Lean.Grind.instLEIntIi :
ToInt.LE Int IntInterval.ii
source
instance Lean.Grind.instLTIntIi :
ToInt.LT Int IntInterval.ii
source
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 }

source
@[simp]
theorem Lean.Grind.toInt_nat (x : Nat) :
↑x = ↑x
source
instance Lean.Grind.instZeroNatCiOfNatInt :
ToInt.Zero Nat (IntInterval.ci 0)
source
instance Lean.Grind.instOfNatNatCiOfNatInt :
ToInt.OfNat Nat (IntInterval.ci 0)
source
instance Lean.Grind.instAddNatCiOfNatInt :
ToInt.Add Nat (IntInterval.ci 0)
source
instance Lean.Grind.instMulNatCiOfNatInt :
ToInt.Mul Nat (IntInterval.ci 0)
source
instance Lean.Grind.instPowNatCiOfNatInt :
ToInt.Pow Nat (IntInterval.ci 0)
source
instance Lean.Grind.instSubNatCiOfNatInt :
ToInt.Sub Nat (IntInterval.ci 0)
source
instance Lean.Grind.instModNatCiOfNatInt :
ToInt.Mod Nat (IntInterval.ci 0)
source
instance Lean.Grind.instDivNatCiOfNatInt :
ToInt.Div Nat (IntInterval.ci 0)
source
instance Lean.Grind.instLENatCiOfNatInt :
ToInt.LE Nat (IntInterval.ci 0)
source
instance Lean.Grind.instLTNatCiOfNatInt :
ToInt.LT Nat (IntInterval.ci 0)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_fin {n : Nat} (x : Fin n) :
↑x = ↑↑x
source
instance Lean.Grind.instZeroFinCoOfNatIntCast {n : Nat} [NeZero n] :
ToInt.Zero (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instOfNatFinCoOfNatIntCast {n : Nat} [NeZero n] :
ToInt.OfNat (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instAddFinCoOfNatIntCast {n : Nat} :
ToInt.Add (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instMulFinCoOfNatIntCast {n : Nat} :
ToInt.Mul (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instModFinCoOfNatIntCast {n : Nat} :
ToInt.Mod (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instDivFinCoOfNatIntCast {n : Nat} :
ToInt.Div (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instLEFinCoOfNatIntCast {n : Nat} :
ToInt.LE (Fin n) (IntInterval.co 0 ↑n)
source
instance Lean.Grind.instLTFinCoOfNatIntCast {n : Nat} :
ToInt.LT (Fin n) (IntInterval.co 0 ↑n)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_uint8 (x : UInt8) :
↑x = ↑x.toNat
source
instance Lean.Grind.instZeroUInt8UintOfNatNat :
ToInt.Zero UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instOfNatUInt8UintOfNatNat :
ToInt.OfNat UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instAddUInt8UintOfNatNat :
ToInt.Add UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instMulUInt8UintOfNatNat :
ToInt.Mul UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instModUInt8UintOfNatNat :
ToInt.Mod UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instDivUInt8UintOfNatNat :
ToInt.Div UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instLEUInt8UintOfNatNat :
ToInt.LE UInt8 (IntInterval.uint 8)
source
instance Lean.Grind.instLTUInt8UintOfNatNat :
ToInt.LT UInt8 (IntInterval.uint 8)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_uint16 (x : UInt16) :
↑x = ↑x.toNat
source
instance Lean.Grind.instZeroUInt16UintOfNatNat :
ToInt.Zero UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instOfNatUInt16UintOfNatNat :
ToInt.OfNat UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instAddUInt16UintOfNatNat :
ToInt.Add UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instMulUInt16UintOfNatNat :
ToInt.Mul UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instModUInt16UintOfNatNat :
ToInt.Mod UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instDivUInt16UintOfNatNat :
ToInt.Div UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instLEUInt16UintOfNatNat :
ToInt.LE UInt16 (IntInterval.uint 16)
source
instance Lean.Grind.instLTUInt16UintOfNatNat :
ToInt.LT UInt16 (IntInterval.uint 16)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_uint32 (x : UInt32) :
↑x = ↑x.toNat
source
instance Lean.Grind.instZeroUInt32UintOfNatNat :
ToInt.Zero UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instOfNatUInt32UintOfNatNat :
ToInt.OfNat UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instAddUInt32UintOfNatNat :
ToInt.Add UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instMulUInt32UintOfNatNat :
ToInt.Mul UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instModUInt32UintOfNatNat :
ToInt.Mod UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instDivUInt32UintOfNatNat :
ToInt.Div UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instLEUInt32UintOfNatNat :
ToInt.LE UInt32 (IntInterval.uint 32)
source
instance Lean.Grind.instLTUInt32UintOfNatNat :
ToInt.LT UInt32 (IntInterval.uint 32)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_uint64 (x : UInt64) :
↑x = ↑x.toNat
source
instance Lean.Grind.instZeroUInt64UintOfNatNat :
ToInt.Zero UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instOfNatUInt64UintOfNatNat :
ToInt.OfNat UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instAddUInt64UintOfNatNat :
ToInt.Add UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instMulUInt64UintOfNatNat :
ToInt.Mul UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instModUInt64UintOfNatNat :
ToInt.Mod UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instDivUInt64UintOfNatNat :
ToInt.Div UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instLEUInt64UintOfNatNat :
ToInt.LE UInt64 (IntInterval.uint 64)
source
instance Lean.Grind.instLTUInt64UintOfNatNat :
ToInt.LT UInt64 (IntInterval.uint 64)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_usize (x : USize) :
↑x = ↑x.toNat
source
instance Lean.Grind.instZeroUSizeUintNumBits :
ToInt.Zero USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instOfNatUSizeUintNumBits :
ToInt.OfNat USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instAddUSizeUintNumBits :
ToInt.Add USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instMulUSizeUintNumBits :
ToInt.Mul USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instModUSizeUintNumBits :
ToInt.Mod USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instDivUSizeUintNumBits :
ToInt.Div USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instLEUSizeUintNumBits :
ToInt.LE USize (IntInterval.uint System.Platform.numBits)
source
instance Lean.Grind.instLTUSizeUintNumBits :
ToInt.LT USize (IntInterval.uint System.Platform.numBits)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_int8 (x : Int8) :
↑x = x.toInt
source
instance Lean.Grind.instZeroInt8SintOfNatNat :
ToInt.Zero Int8 (IntInterval.sint 8)
source
instance Lean.Grind.instOfNatInt8SintOfNatNat :
ToInt.OfNat Int8 (IntInterval.sint 8)
source
instance Lean.Grind.instAddInt8SintOfNatNat :
ToInt.Add Int8 (IntInterval.sint 8)
source
instance Lean.Grind.instMulInt8SintOfNatNat :
ToInt.Mul Int8 (IntInterval.sint 8)
source
instance Lean.Grind.instLEInt8SintOfNatNat :
ToInt.LE Int8 (IntInterval.sint 8)
source
instance Lean.Grind.instLTInt8SintOfNatNat :
ToInt.LT Int8 (IntInterval.sint 8)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_int16 (x : Int16) :
↑x = x.toInt
source
instance Lean.Grind.instZeroInt16SintOfNatNat :
ToInt.Zero Int16 (IntInterval.sint 16)
source
instance Lean.Grind.instOfNatInt16SintOfNatNat :
ToInt.OfNat Int16 (IntInterval.sint 16)
source
instance Lean.Grind.instAddInt16SintOfNatNat :
ToInt.Add Int16 (IntInterval.sint 16)
source
instance Lean.Grind.instMulInt16SintOfNatNat :
ToInt.Mul Int16 (IntInterval.sint 16)
source
instance Lean.Grind.instLEInt16SintOfNatNat :
ToInt.LE Int16 (IntInterval.sint 16)
source
instance Lean.Grind.instLTInt16SintOfNatNat :
ToInt.LT Int16 (IntInterval.sint 16)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_int32 (x : Int32) :
↑x = x.toInt
source
instance Lean.Grind.instZeroInt32SintOfNatNat :
ToInt.Zero Int32 (IntInterval.sint 32)
source
instance Lean.Grind.instOfNatInt32SintOfNatNat :
ToInt.OfNat Int32 (IntInterval.sint 32)
source
instance Lean.Grind.instAddInt32SintOfNatNat :
ToInt.Add Int32 (IntInterval.sint 32)
source
instance Lean.Grind.instMulInt32SintOfNatNat :
ToInt.Mul Int32 (IntInterval.sint 32)
source
instance Lean.Grind.instLEInt32SintOfNatNat :
ToInt.LE Int32 (IntInterval.sint 32)
source
instance Lean.Grind.instLTInt32SintOfNatNat :
ToInt.LT Int32 (IntInterval.sint 32)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_int64 (x : Int64) :
↑x = x.toInt
source
instance Lean.Grind.instZeroInt64SintOfNatNat :
ToInt.Zero Int64 (IntInterval.sint 64)
source
instance Lean.Grind.instOfNatInt64SintOfNatNat :
ToInt.OfNat Int64 (IntInterval.sint 64)
source
instance Lean.Grind.instAddInt64SintOfNatNat :
ToInt.Add Int64 (IntInterval.sint 64)
source
instance Lean.Grind.instMulInt64SintOfNatNat :
ToInt.Mul Int64 (IntInterval.sint 64)
source
instance Lean.Grind.instLEInt64SintOfNatNat :
ToInt.LE Int64 (IntInterval.sint 64)
source
instance Lean.Grind.instLTInt64SintOfNatNat :
ToInt.LT Int64 (IntInterval.sint 64)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_bitVec {v : Nat} (x : BitVec v) :
↑x = ↑x.toNat
source
instance Lean.Grind.instZeroBitVecUint {v : Nat} :
ToInt.Zero (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instOfNatBitVecUint {v : Nat} :
ToInt.OfNat (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instAddBitVecUint {v : Nat} :
ToInt.Add (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instMulBitVecUint {v : Nat} :
ToInt.Mul (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instModBitVecUint {v : Nat} :
ToInt.Mod (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instDivBitVecUint {v : Nat} :
ToInt.Div (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instLEBitVecUint {v : Nat} :
ToInt.LE (BitVec v) (IntInterval.uint v)
source
instance Lean.Grind.instLTBitVecUint {v : Nat} :
ToInt.LT (BitVec v) (IntInterval.uint v)
source
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 := ⋯ }

source
@[simp]
theorem Lean.Grind.toInt_isize (x : ISize) :
↑x = x.toInt
source
instance Lean.Grind.instZeroISizeSintNumBits :
ToInt.Zero ISize (IntInterval.sint System.Platform.numBits)
source
instance Lean.Grind.instOfNatISizeSintNumBits :
ToInt.OfNat ISize (IntInterval.sint System.Platform.numBits)
source
instance Lean.Grind.instAddISizeSintNumBits :
ToInt.Add ISize (IntInterval.sint System.Platform.numBits)
source
instance Lean.Grind.instMulISizeSintNumBits :
ToInt.Mul ISize (IntInterval.sint System.Platform.numBits)
source
instance Lean.Grind.instLEISizeSintNumBits :
ToInt.LE ISize (IntInterval.sint System.Platform.numBits)
source
instance Lean.Grind.instLTISizeSintNumBits :
ToInt.LT ISize (IntInterval.sint System.Platform.numBits)