module Juvix.Builtin.V1.Trait.Natural;

import Juvix.Builtin.V1.Nat.Base open using {Nat};
import Juvix.Builtin.V1.Fixity open;

trait
type Natural A :=
  mkNatural {
    syntax operator + additive;
    + : A -> A -> A;
    syntax operator * multiplicative;
    * : A -> A -> A;
    builtin from-nat
    fromNat : Nat -> A
  };

open Natural public;