module Juvix.Builtin.V1.Trait.Natural;

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

trait
type Natural A :=
  mkNatural@{
    {{FromNaturalI}} : FromNatural A;
    syntax operator + additive;
    {-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-}
    + : A -> A -> A;
    syntax operator * multiplicative;
    {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
    * : A -> A -> A;
  };

open Natural public;