module IEEE754.Sign where open import IEEE754.Prelude data Sign : Type₀ where positive : Sign negative : Sign negateSign : Sign → Sign negateSign positive = negative negateSign negative = positive signBit : Sign → Bit signBit positive = bit0 signBit negative = bit1 bitSign : Bit → Sign bitSign false = positive bitSign true = negative bitSign-signBit : (s : Sign) → bitSign (signBit s) ≡ s bitSign-signBit positive = refl bitSign-signBit negative = refl signBit-bitSign : (b : Bit) → signBit (bitSign b) ≡ b signBit-bitSign false = refl signBit-bitSign true = refl negateSign-involutive : (s : Sign) → negateSign (negateSign s) ≡ s negateSign-involutive positive = refl negateSign-involutive negative = refl