module Stdlib.Data.Nat;
import Juvix.Builtin.V1.Nat open public;
import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
import Stdlib.Data.Nat.Base as Nat;
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.DivMod open public;
import Stdlib.Data.Nat.Ord as Nat;
--- 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;
instance
eqNatI : Eq Nat := mkEq (Nat.==);
instance
ordNatI : Ord Nat := mkOrd Nat.compare;
instance
showNatI : Show Nat := mkShow natToString;
instance
divModNatI : DivMod Nat :=
mkDivMod@{
div := Nat.div;
mod := Nat.mod
};
Last modified on 2024-07-11 16:35 UTC