module Stdlib.Data.Nat;

import Juvix.Builtin.V1.Nat open hiding {module Nat} public;
import Stdlib.Data.Nat.Base open hiding {module Nat; +; *; div; mod} public;

module Nat;
  open Stdlib.Data.Nat.Base.Nat public;

  import Stdlib.Data.Nat.Base open public;
  import Stdlib.Data.Nat.Ord open public;
end;

import Stdlib.Data.String.Base open;

import Stdlib.Trait.Eq open public;
import Stdlib.Trait.Ord open public;
import Stdlib.Trait.Show open public;
import Stdlib.Trait.Natural open public;
import Stdlib.Trait.FromNatural open public;
import Stdlib.Trait.DivMod open public;

--- Converts a ;Nat; into a ;String;.
builtin nat-to-string
axiom natToString : Nat -> String;

--- Partial function that converts a ;String; into a ;Nat;.
builtin string-to-nat
axiom stringToNat : String -> Nat;

{-# specialize: true, inline: case #-}
instance
eqNatI : Eq Nat := mkEq (Nat.==);

{-# specialize: true, inline: case #-}
instance
ordNatI : Ord Nat := mkOrd Nat.compare;

instance
showNatI : Show Nat := mkShow natToString;

{-# specialize: true, inline: case #-}
instance
divModNatI : DivMod Nat :=
  mkDivMod@{
    div := Nat.div;
    mod := Nat.mod;
  };