def Hex.Int.signImpl (z : Int) : Int

Integer sign using comparisons with zero. Compiled comparisons inspect the integer's sign and size without copying its multiprecision magnitude.

Equations

• Hex.Int.signImpl z = if z < 0 then -1 else if z = 0 then 0 else 1

theorem Hex.Int.signImpl_eq : signImpl = Int.sign

The comparison implementation preserves the integer sign at every input.

@[csimp]

theorem Hex.Int.sign_eq_signImpl : Int.sign = signImpl

Compile integer sign through zero comparisons. In the current toolchain, the constructor-based implementation copies positive multiprecision integers when it converts their magnitude to a natural number.