module Juvix.Builtin.V1.Trait.FromNatural;

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

trait
type FromNatural A := mkFromNatural@{builtin from-nat fromNat : Nat -> A};

open FromNatural public;