    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Showing integers
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Integer.Show where

    open import Data.Integer.Base using (ℤ; +_; -[1+_])
    open import Data.Nat.Base using (suc)
    open import Data.Nat.Show using () renaming (show to showℕ)
    open import Data.String.Base using (String; _++_)

    ------------------------------------------------------------------------
    -- Show

    -- Decimal notation
    -- Time complexity is O(log₁₀(n))

    show : ℤ → String
    show (+ n)    = showℕ n
    show -[1+ n ] = "-" ++ showℕ (suc n)