Lean4
/-- Alternative representation of integers using a sign bit at the end.
The convention on sign here is to have the argument to `msb` denote
the sign of the MSB itself, with all higher bits set to the negation
of this sign. The result is interpreted in two's complement.
13 = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true))))
-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))
As with `Num`, a special case must be added for zero, which has no msb,
but by two's complement symmetry there is a second special case for -1.
Here the `Bool` field indicates the sign of the number.
0 = ..0000000(base 2) = zero false
-1 = ..1111111(base 2) = zero true -/
inductive SNum : Type
| zero : Bool → SNum
| nz : NzsNum → SNum
deriving DecidableEq
