------------------------------------------------------------------------
-- 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₂