------------------------------------------------------------------------
-- The Agda standard library
--
-- Signs
------------------------------------------------------------------------

module Data.Sign where

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (yes; no)

-- Signs.

data Sign : Set where
  - : Sign
  + : Sign

-- Decidable equality.

infix 4 _≟_

_≟_ : Decidable {A = Sign} _≡_
-  - = yes refl
-  + = no λ()
+  - = no λ()
+  + = yes refl

-- The opposite sign.

opposite : Sign  Sign
opposite - = +
opposite + = -

-- "Multiplication".

infixl 7 _*_

_*_ : Sign  Sign  Sign
+ * s₂ = s₂
- * s₂ = opposite s₂