[ new ] module Data.Sign.Show (#2627)

Author: gallais

CHANGELOG.md

@@ -103,6 +103,8 @@ New modules
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
+* `Data.Sign.Show` to show a sign
+
 Additions to existing modules
 -----------------------------
 

src/Data/Sign/Show.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing signs
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sign.Show where
+
+open import Data.Sign.Base using (Sign; +; -)
+open import Data.String.Base using (String)
+
+show : Sign → String
+show + = "+"
+show - = "-"