module Stdlib.Data.Nat;
open import Stdlib.Data.Nat.Base public;
open import Stdlib.Data.String.Base;
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.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;
module NatTraits;
Eq : Eq Nat;
Eq := Eq.mkEq (Nat.==);
Ord : Ord Nat;
Ord := Ord.mkOrd Nat.compare;
Show : Show Nat;
Show := Show.mkShow natToString;
end;
Last modified on 2023-05-08 11:40 UTC