stdlib - 0.0.1

Juvix.Builtin.V1.Trait.Natural

Description

Definitions

trait type Natural ASource#

Constructors

| mkNatural { syntax operator + additive; + : A -> A -> A; syntax operator * multiplicative; * : A -> A -> A; builtin from-nat fromNat : Nat -> A }

open Natural public