diff options
Diffstat (limited to 'backends/lean/Base/Primitives/Scalar.lean')
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 48 |
1 files changed, 27 insertions, 21 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 1e9b51c2..3beb7527 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -66,27 +66,33 @@ def U128.smin : Int := 0 def U128.smax : Int := HPow.hPow 2 128 - 1 -- The "normalized" bounds, that we use in practice -def I8.min := -128 -def I8.max := 127 -def I16.min := -32768 -def I16.max := 32767 -def I32.min := -2147483648 -def I32.max := 2147483647 -def I64.min := -9223372036854775808 -def I64.max := 9223372036854775807 -def I128.min := -170141183460469231731687303715884105728 -def I128.max := 170141183460469231731687303715884105727 -@[simp] def U8.min := 0 -def U8.max := 255 -@[simp] def U16.min := 0 -def U16.max := 65535 -@[simp] def U32.min := 0 -def U32.max := 4294967295 -@[simp] def U64.min := 0 -def U64.max := 18446744073709551615 -@[simp] def U128.min := 0 -def U128.max := 340282366920938463463374607431768211455 -@[simp] def Usize.min := 0 +def I8.min : Int := -128 +def I8.max : Int := 127 +def I16.min : Int := -32768 +def I16.max : Int := 32767 +def I32.min : Int := -2147483648 +def I32.max : Int := 2147483647 +def I64.min : Int := -9223372036854775808 +def I64.max : Int := 9223372036854775807 +def I128.min : Int := -170141183460469231731687303715884105728 +def I128.max : Int := 170141183460469231731687303715884105727 +@[simp] +def U8.min : Int := 0 +def U8.max : Int := 255 +@[simp] +def U16.min : Int := 0 +def U16.max : Int := 65535 +@[simp] +def U32.min : Int := 0 +def U32.max : Int := 4294967295 +@[simp] +def U64.min : Int := 0 +def U64.max : Int := 18446744073709551615 +@[simp] +def U128.min : Int := 0 +def U128.max : Int := 340282366920938463463374607431768211455 +@[simp] +def Usize.min : Int := 0 def Isize.refined_min : { n:Int // n = I32.min ∨ n = I64.min } := ⟨ Isize.smin, by |