    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Integers
    ------------------------------------------------------------------------

    -- See README.Data.Integer for examples of how to use and reason about
    -- integers.

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

    module Data.Integer where

    ------------------------------------------------------------------------
    -- Re-export basic definition, operations and queries

    open import Data.Integer.Base public
    open import Data.Integer.Properties public
      using (_≟_; _≤?_; _<?_)

    ------------------------------------------------------------------------
    -- Deprecated

    -- Version 0.17

    open import Data.Integer.Properties public
      using (◃-cong; drop‿+≤+; drop‿-≤-)
      renaming (◃-inverse to ◃-left-inverse)

    -- Version 1.5
    -- Show

    import Data.Nat.Show as ℕ using (show)
    open import Data.Sign.Base as Sign using (Sign)
    open import Data.String.Base using (String; _++_)

    show : ℤ → String
    show i = showSign (sign i) ++ ℕ.show ∣ i ∣
      where
      showSign : Sign → String
      showSign Sign.- = "-"
      showSign Sign.+ = ""

    {-# WARNING_ON_USAGE show
    "Warning: show was deprecated in v1.5.
    Please use Data.Integer.Show's show instead."
    #-}