{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
module Agda.Builtin.Int where
 
open import Agda.Builtin.Nat
open import Agda.Builtin.String
 
infix  pos  -- Standard library uses this as +_
 
data Int : Set where
  pos    : (n : Nat) → Int
  negsuc : (n : Nat) → Int
 
{-# BUILTIN INTEGER       Int    #-}
{-# BUILTIN INTEGERPOS    pos    #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}
 
primitive primShowInteger : Int → String