module Stdlib.Data.Int;

open import Stdlib.Data.Int.Base public;

import Stdlib.Data.Nat as Nat;
open Nat using {Nat;suc;zero;sub};
open import Stdlib.Data.String;
open import Stdlib.Data.Bool;

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

import Stdlib.Trait.Ord as Ord;
open Ord using {Ord};

import Stdlib.Trait.Show as Show;
open Show using {Show};

import Stdlib.Data.Int.Ord as Int;

--- Converts an ;Int; into ;String;.
builtin int-to-string
axiom intToString : Int -> String;

module IntTraits;
  Eq : Eq Int;
  Eq := Eq.mkEq (Int.==);
  
  Ord : Ord Int;
  Ord := Ord.mkOrd Int.compare;
  
  Show : Show Int;
  Show := Show.mkShow intToString;
end;
Last modified on 2023-05-08 11:40 UTC