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;Last modified on 2024-07-11 16:35 UTC