module Juvix.Builtin.V1.Nat;

import Juvix.Builtin.V1.Trait.Natural open public;
import Juvix.Builtin.V1.Nat.Base open hiding {+; *; div; mod} public;
import Juvix.Builtin.V1.Nat.Base as Nat;

{-# specialize: true, inline: case #-}
instance
naturalNatI : Natural Nat :=
  mkNatural@{
    + := (Nat.+);
    * := (Nat.*);
    div := Nat.div;
    mod := Nat.mod;
    fromNat (x : Nat) : Nat := x
  };