------------------------------------------------------------------------
-- The Agda standard library
--
-- Integer Literals
------------------------------------------------------------------------

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

module Data.Integer.Literals where

open import Agda.Builtin.FromNat using (Number)
open import Agda.Builtin.FromNeg using (Negative)
open import Data.Unit.Base using (⊤)
open import Data.Integer.Base using (ℤ; -_; +_)

number : Number ℤ
number = record
  { Constraint = λ _ → ⊤
  ; fromNat    = λ n → + n
  }

negative : Negative ℤ
negative = record
  { Constraint = λ _ → ⊤
  ; fromNeg    = λ n → - (+ n)
  }