------------------------------------------------------------------------
-- 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."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4